Fixed Composition in an Actual Clifford History Fiber

Abstract

A positive natural composition and a single actual Clifford history are jointly realizable exactly when the rational quarter-counts are integral, all eight integer edge counts are nonnegative, and their undirected positive support is connected to the initial state 00.

Source is the native FreeMagma Bool: true denotes alpha, false beta. The source remains a nonempty ordered binary tree, with its brackets retained. Substitution sends alpha to beta and beta to the ordered pair (beta,alpha). Composition counts the leaves of each label.

The carrier is the actual real CliffordAlgebra for Q(a,b)=aa+ab-bb. A and B are the canonical vector images. E multiplies their images in original leaf order; W3(t)=(E(t),E(rho(t)),E(rho(rho(t)))). S=BA, D=A+B, g=(A,B,S), h=(B,S,D), and R00=1, R10=g, R01=h, R11=gh. L(u,v,w)=((-1)^vS^(2u),(-1)^wS^(2v),(-1)^uS^(2w)).

Write phi for the real golden ratio and psi for its conjugate. The notation mat(a,b,c,d) lists a two-by-two real matrix in row order.

Definition 1.1 (Golden-ratio vector representation).

$$\forall a\in \mathbb{R},\forall b\in \mathbb{R},K\left((a,b)\right)=\mathrm{mat}\left(0,a+b\cdot phi,a+b\cdot psi,0\right)$$

Formalization. D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.K (✓ std3).

Source. Repository-derived.

Commentary.

K is real linear and sends the two coordinate vectors to off-diagonal matrices.

Theorem 1.2 (Quadratic relation).

$$\forall x\in \mathbb{R}\times \mathbb{R},K\left(x\right)\cdot K\left(x\right)=\mathrm{algebraMap}\left(Q\left(x\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.k_square (✓ std3). ∎

Source. Repository-derived.

Commentary.

The scalar algebra map has target the two-by-two real matrix algebra.

Definition 1.3 (Clifford matrix representation).

$$sep=\mathrm{CliffordLift}\left(Q,K\right)$$

Formalization. D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.sep (✓ std3).

Source. Repository-derived.

Commentary.

The quadratic relation extends K to a real algebra homomorphism from C.

Theorem 1.4 (Image of the alpha vector).

$$\mathrm{sep}\left(A\right)=\mathrm{mat}\left(0,1,1,0\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.sep_a (✓ std3). ∎

Source. Repository-derived.

Commentary.

The alpha image exchanges the two matrix coordinates.

Theorem 1.5 (Image of the beta vector).

$$\mathrm{sep}\left(B\right)=\mathrm{mat}\left(0,phi,psi,0\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.sep_b (✓ std3). ∎

Source. Repository-derived.

Commentary.

The beta image uses the two conjugate roots in its off-diagonal entries.

Theorem 1.6 (Complete same-source criterion).

$$\forall u\in \mathbb{Z},\forall v\in \mathbb{Z},\forall w\in \mathbb{Z},\forall p\in \left\{0,1\right\},\forall q\in \left\{0,1\right\},\forall ac\in \mathbb{N},\forall bc\in \mathbb{N},1\le ac+bc\Rightarrow \left(\left(\exists t\in Source,\left(W_3\right)\left(t\right)=L\left(u,v,w\right)\cdot R_{(p,q)}\wedge c\left(t\right)=(ac,bc)\right)\iff \left(\exists X\in \mathbb{Z},\exists Y\in \mathbb{Z},\left(\left(X=\frac{ac-p-2\cdot w+2\cdot u}{4}\wedge Y=\frac{bc-q-2\cdot u+2\cdot v}{4}\right)\wedge \left(\forall e\in (\left\{0,1\right\}\times \left\{0,1\right\})\times \left\{0,1\right\},0\le \mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(e\right)\right)\right)\wedge \left(\forall e\in (\left\{0,1\right\}\times \left\{0,1\right\})\times \left\{0,1\right\},0<\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(e\right)\Rightarrow \left(\mathrm{Nonempty}\left(\mathrm{Path}\left(\mathrm{Symmetrify}\left(\mathrm{PositiveSupport}\left(\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\right)\right),(0,0),\mathrm{src}\left(e\right)\right)\right)\wedge \mathrm{Nonempty}\left(\mathrm{Path}\left(\mathrm{Symmetrify}\left(\mathrm{PositiveSupport}\left(\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\right)\right),(0,0),\mathrm{step}\left(\mathrm{src}\left(e\right),\mathrm{label}\left(e\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

All u,v,w are integers; p,q are Boolean bits interpreted as 0 or 1. All ac,bc are natural numbers with ac+bc>=1; either coordinate may be zero. Criterion means that the rational numbers X=(ac-p-2w+2u)/4 and Y=(bc-q-2u+2v)/4 have integer witnesses, all eight counts below are nonnegative, and every endpoint of every positive-count edge is connected to 00 in the undirected positive support. Unused ambient vertices impose no connectivity requirement.

The alpha counts at departures 00,10,01,11 are X+w-u+p, X+w, X, X-u. The beta counts at departures 00,01,10,11 are Y+u+q*(1-p), Y, Y-v+p*q, Y+u-v. Alpha toggles the first bit; beta toggles the second.

$\begin{array}{r}{x}_{00}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((0,0),1)\right)=X+w-u+p\\ x_{10}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((1,0),1)\right)=X+w\\ x_{01}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((0,1),1)\right)=X\\ x_{11}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((1,1),1)\right)=X-u\\ y_{00}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((0,0),0)\right)=Y+u+q\cdot \left(1-p\right)\\ y_{01}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((0,1),0)\right)=Y\\ y_{10}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((1,0),0)\right)=Y-v+p\cdot q\\ y_{11}=\mathrm{edgeCounts}\left(u,v,w,X,Y,p,q\right)\left(((1,1),0)\right)=Y+u-v\end{array}$

In the displayed criterion, Kind=State times the Boolean leaf label, src and label are its two projections, and Path is the finite quiver path type. The label 1 denotes alpha and 0 denotes beta. Symmetrify allows each positive edge in either direction; a zero-length path retains the initial vertex 00. The positive support and its step function are specified by:

$\begin{array}{r}State=\left\{0,1\right\}\times \left\{0,1\right\}\\ Kind=(\left\{0,1\right\}\times \left\{0,1\right\})\times \left\{0,1\right\}\\ \forall z\in \left\{0,1\right\}\times \left\{0,1\right\},\forall b\in \left\{0,1\right\},\mathrm{src}\left((z,b)\right)=z\wedge \mathrm{label}\left((z,b)\right)=b\\ \forall r\in \left\{0,1\right\},\forall s\in \left\{0,1\right\},\mathrm{step}\left((r,s),1\right)=(1-r,s)\wedge \mathrm{step}\left((r,s),0\right)=(r,1-s)\\ \forall m\in (\left\{0,1\right\}\times \left\{0,1\right\})\times \left\{0,1\right\}\to \mathbb{Z},\forall s\in \left\{0,1\right\}\times \left\{0,1\right\},\forall z\in \left\{0,1\right\}\times \left\{0,1\right\},\mathrm{Nonempty}\left(\mathrm{Hom}\left(\mathrm{PositiveSupport}\left(m\right),s,z\right)\right)\iff \left(\exists b\in \left\{0,1\right\},\mathrm{step}\left(s,b\right)=z\wedge 0<m\left((s,b)\right)\right)\end{array}$

The integer witness equations are ac=4X+2w-2u+p and bc=4Y+2u-2v+q, proved equivalent to the rational quotients. A maximum path whose edge counts are bounded by the capacities reaches the prescribed terminal by its residual divergence. Any remaining capacity is balanced. A boundary crossing in the original weak support supplies a visited splice vertex; a nonempty residual closed path would increase the maximum length. Residual connectivity is not assumed.

The same chronological path supplies the leaf word, all three actual Clifford coordinates and the composition. Necessity identifies parameters by actual Clifford reflection, and sufficiency brackets that same nonempty word into an actual Source. Parallel occurrences are retained by their exact chronological counts. Flow balance alone is insufficient: unit history at composition (4,0) gives two disconnected alpha cycles.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.K
• Truth anchor: D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.k_square
• Truth anchor: D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.result
• Truth anchor: D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.sep
• Truth anchor: D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.sep_a
• Truth anchor: D5/S3/Arith/FibonacciAtomic/FixedHistoryComposition.sep_b
• Dependency: D5/S3/Arith/FibonacciAtomic/GenealogicalFiberTransport