Native Rotation and Complete Fiber Depth Extrema

Abstract

One contextual rotation attains the entire Fibonacci word and geometry fiber depth range.

S is the actual FreeMagma Bool source: finite nonempty ordered binary trees. Alpha is the true leaf, beta the false leaf, and pair retains the original ordered brackets. The original substitution rho sends alpha to beta and beta to pair(beta,alpha). R(k,t) is its k-fold iterate, including k=0. T(n)=R(n,alpha); U(n) is the existing AncestorAreaInstability.rotated(n-3), with U(3)=pair(beta,pair(alpha,beta)). T(3)=pair(pair(beta,alpha),beta). The word w(t)=wd(t) retains every labelled leaf in its original order; ell(t) counts all leaves. G is the original five-coordinate geometry of that whole word. Depth and Q are the original intrinsic substitution coordinates, with Boolean true written 1 and false written 0.

Definition 1.1 (One Contextual Associativity Step).

$$\forall C:\mathrm{OutputContext}\left(\right),(\forall s:S,(\forall t:S,((\mathrm{ContextRotation}\left(C,s,t\right))⟺(\exists a:S,(\exists b:S,(\exists c:S,((s=\mathrm{plug}\left(C,\mathrm{pair}\left(\mathrm{pair}\left(a,b\right),c\right)\right))\wedge (t=\mathrm{plug}\left(C,\mathrm{pair}\left(a,\mathrm{pair}\left(b,c\right)\right)\right)))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.ContextRotation (✓ std3).

Source. Repository-derived.

Commentary.

C is the existing ActualLeafHistoryRigidity.OutputContext. Plugging its unique hole preserves every ordered sibling and label. ContextRotation uses one local associativity move.

Definition 1.2 (Actual Undirected Rotation Graph).

$$\forall s:S,(\forall t:S,((\mathrm{Adj}\left(s,t\right))⟺((s\ne t)\wedge (\exists C:\mathrm{OutputContext}\left(\right),((\mathrm{ContextRotation}\left(C,s,t\right))\vee (\mathrm{ContextRotation}\left(C,t,s\right)))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.rotationGraph (✓ std3).

Source. Repository-derived.

Commentary.

The graph has the entire actual source as its vertex set. Its edges are either orientation of a contextual ordered associativity step between distinct sources. d is the ordinary SimpleGraph.dist and Reachable is graph reachability. For disconnected pairs ordinary distance is zero; the universal metric claim retains Reachable.

Definition 1.3 (Native Left Context).

$$(C\left(0\right)=\mathrm{hole}\left(\right))\wedge (\forall k:\mathrm{Nat}\left(\right),(C\left(k+1\right)=\mathrm{left}\left(C\left(k\right),T\left(k+2\right)\right)))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.leftContext (✓ std3).

Source. Repository-derived.

Commentary.

C(k) denotes leftContext(k). Its right siblings are the original T(k+2), while its hole follows k left edges. In addresses false means left.

Theorem 1.4 (Single Rotation, Forward Transport, and Sharp Complete Fiber Bounds).

$$(\forall n:\mathrm{Nat}\left(\right),((3\le n)⟹((\mathrm{holeAddress}\left(C\left(n-3\right)\right)=\mathrm{replicate}\left(n-3,0\right))\wedge (\mathrm{plug}\left(C\left(n-3\right),T\left(3\right)\right)=T\left(n\right))\wedge (\mathrm{plug}\left(C\left(n-3\right),U\left(3\right)\right)=U\left(n\right))\wedge (\mathrm{ContextRotation}\left(C\left(n-3\right),T\left(n\right),U\left(n\right)\right))\wedge (\mathrm{Adj}\left(T\left(n\right),U\left(n\right)\right))\wedge (d\left(T\left(n\right),U\left(n\right)\right)=1)\wedge (w\left(T\left(n\right)\right)=w\left(U\left(n\right)\right))\wedge (\mathrm{ell}\left(T\left(n\right)\right)=\mathrm{fib}\left(n+1\right))\wedge (\mathrm{ell}\left(U\left(n\right)\right)=\mathrm{fib}\left(n+1\right))\wedge (Q\left(T\left(n\right)\right)=(n,1))\wedge (Q\left(U\left(n\right)\right)=(0,0))\wedge (\forall j:\mathrm{Nat}\left(\right),((w\left(R\left(j,T\left(n\right)\right)\right)=w\left(R\left(j,U\left(n\right)\right)\right))\wedge (G\left(w\left(R\left(j,T\left(n\right)\right)\right)\right)=G\left(w\left(R\left(j,U\left(n\right)\right)\right)\right))\wedge (\mathrm{depth}\left(R\left(j,T\left(n\right)\right)\right)=n+j)\wedge (\mathrm{depth}\left(R\left(j,U\left(n\right)\right)\right)=j)))\wedge (\forall s:S,((w\left(s\right)=w\left(T\left(n\right)\right))⟹((0\le \mathrm{depth}\left(s\right))\wedge (\mathrm{depth}\left(s\right)\le n))))\wedge (\forall s:S,((G\left(w\left(s\right)\right)=G\left(w\left(T\left(n\right)\right)\right))⟹((0\le \mathrm{depth}\left(s\right))\wedge (\mathrm{depth}\left(s\right)\le n))))\wedge (\mathrm{depth}\left(T\left(n\right)\right)=n)\wedge (\mathrm{depth}\left(U\left(n\right)\right)=0))))\wedge (\neg (\exists A:\mathrm{Real}\left(\right),(\forall s:S,(\forall t:S,((w\left(s\right)=w\left(t\right))⟹((\mathrm{Reachable}\left(s,t\right))⟹(|\mathrm{real}\left(\mathrm{depth}\left(s\right)\right)-\mathrm{real}\left(\mathrm{depth}\left(t\right)\right)|\le (A)\cdot (\mathrm{real}\left(d\left(s,t\right)\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.native_rotation_depth_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

The structural induction on C(k) uses the source centralizer recurrence T(k+4)=pair(T(k+3),T(k+2)). It identifies C(k).plug(T(3)) with T(k+3) and C(k).plug(U(3)) with rotated(k), at the exact address L repeated k times. Thus the original three-leaf reassociation remains one edge at every n>=3. The existing AncestorAreaInstability.result supplies the whole-word equality, Fibonacci leaf count and the two endpoint depths. Unequal depths make the sources distinct, so adjacency gives distance exactly one.

The existing intrinsic coordinate composites identify the ray flag and supply the one-step coordinate transport. Iteration gives depths n+j and j. The original GeometryEntranceRatio.wd_substitution gives w(rho(t))=sigma(w(t)), so every common forward iterate has the same entire labelled word and hence the same G. No rotation-distance assertion is made about these common forward iterates.

For every actual ancestor p and exponent k, the composition transport and Fibonacci recurrence give ell(R(k,p))=fib(k+1) composition(p).1 + fib(k+2) composition(p).2, at least fib(k+1) because ell(p)>0. Applying this estimate to the realized maximal ancestor bounds every actual tree of length fib(n+1) by depth n, using strict Fibonacci growth for n>=3. Same words have the same length by FreeMagma.length_toFreeSemigroup. The original GeometryEntranceRatio.tree_length also fixes the length of every member of the complete same-G fiber. Both fibers therefore have minimum zero and maximum n, attained by these same U(n) and T(n). There is no restriction to the displayed family, selected shapes, or selected word representatives.

If a finite real coefficient A bounded depth differences for all same-word reachable pairs, these distance-one witnesses would give n<=A for every n>=3, contradicting unbounded natural numbers. The result connects native contextual rotation with the intrinsic depth coordinate. It is a repository-derived synthesis of the cited family and coordinate results, with no global priority claim, quotient adjacency, physical acquisition claim, or bound for arbitrary non-Fibonacci leaf counts.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.ContextRotation
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.leftContext
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.native_rotation_depth_gap
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap.rotationGraph
• Dependency: D5/S3/Arith/FibonacciAtomic/ActualLeafHistoryRigidity
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/ActualObserverAbsorbingNormalization
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/IntrinsicSubstitutionCoordinates