Actual Fibonacci support chain

Abstract

ActualFibonacciSupportChain

Sources are finite nonempty ordered Boolean trees. False addresses mean left and true addresses mean right. The initial source is the true-labelled leaf alpha, and substitution sends alpha to beta and beta to the ordered pair of beta and alpha. Pos denotes the set of all literal addresses whose native readout is not absent; it records only presence, without requiring agreement of leaf labels or branch replies.

Theorem 1.1 (Strict inclusions and bounded support agreement).

$$\forall k:Nat,((1\le k)⟹(((\mathrm{Pos}\left(\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right)\right)\subseteq \mathrm{Pos}\left(\mathrm{iterate}\left(substitution,2k+1,\mathrm{of}\left(true\right)\right)\right))\wedge (\mathrm{Pos}\left(\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right)\right)\ne \mathrm{Pos}\left(\mathrm{iterate}\left(substitution,2k+1,\mathrm{of}\left(true\right)\right)\right)))\wedge ((\mathrm{Pos}\left(\mathrm{iterate}\left(substitution,2k+1,\mathrm{of}\left(true\right)\right)\right)\subseteq \mathrm{Pos}\left(\mathrm{mul}\left(\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right),\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right)\right)\right))\wedge (\mathrm{Pos}\left(\mathrm{iterate}\left(substitution,2k+1,\mathrm{of}\left(true\right)\right)\right)\ne \mathrm{Pos}\left(\mathrm{mul}\left(\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right),\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right)\right)\right)))\wedge (\forall q:Address,((\mathrm{length}\left(q\right)\le k)⟹(((\mathrm{readout}\left(q,\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right)\right)\ne absent)⟺(\mathrm{readout}\left(q,\mathrm{iterate}\left(substitution,2k+1,\mathrm{of}\left(true\right)\right)\right)\ne absent))\wedge ((\mathrm{readout}\left(q,\mathrm{iterate}\left(substitution,2k+1,\mathrm{of}\left(true\right)\right)\right)\ne absent)⟺(\mathrm{readout}\left(q,\mathrm{mul}\left(\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right),\mathrm{iterate}\left(substitution,2k,\mathrm{of}\left(true\right)\right)\right)\right)\ne absent)))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/ActualFibonacciSupportChain.actual_fibonacci_support_chain (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural k at least one, the support of the even orbit tree is strictly contained in the next odd support, which is strictly contained in the support of the ordered pair of two copies of the even tree. Both adjacent membership equivalences hold at every address of length at most k, including the empty address.

The orbit recurrence gives left and right children with ranks one and two below the parent rank. Induction on an arbitrary address proves that every address of length d is present at every orbit rank at least twice d. Applying this fact to rank twice k makes all three support bits equal to one throughout the stated radius. Original subtree transport gives the global inclusions. The words consisting of k minus one right edges followed by two left edges, and of k right edges followed by one left edge, respectively establish strictness.

The statement has no source-size bound, selected-word restriction or image-positivity premise. It concerns support bits on the actual trees; it gives neither complete reply equality nor a protocol cost bound.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/ActualFibonacciSupportChain.actual_fibonacci_support_chain
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/DelayedOriginalReadout
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeDepthPatterns
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceTransportCentralizer