Every missing-prefix actual obstruction

Abstract

Every missing-prefix actual obstruction

The original height is the ordered-tree depth with leaves at zero. Family D consists exactly of outer(v)=pair(alpha,v) with height(v)<=D. PublicMenu prefixes each relative literal by R in the original order. The whole-vector identity holds at every natural update count, including blocked suffixes.

For a missing proper prefix a and selected q=ar with r nonempty, use exactly v=spine(a,alpha), vprime=spine(a,beta). The spine is the original FM.21 context. Its height is length(a), and flipping its reached leaf at a produces the other tree. The existing off-leaf flip invariance therefore supplies equality of every selected initial coordinate.

Take one common k=pathCost(r)+1. Atomic navigation reaches beta from alpha and a branch from beta at r. Originally-present transport is applied at a, then the literal append identity transfers those replies to q. It is never applied at initially absent q. The bound length(q)+1<=D makes k<2D and forces D>=2. At D=1 no such missing-prefix case exists.

Theorem 1.1 (A common atomic separating count at each address).

$$\forall r:Address,((\mathrm{readout}\left(r,\mathrm{iterate}\left(substitution,\mathrm{pathCost}\left(r\right)+1,\mathrm{of}\left(true\right)\right)\right)=beta)\wedge (\mathrm{readout}\left(r,\mathrm{iterate}\left(substitution,\mathrm{pathCost}\left(r\right)+1,\mathrm{of}\left(false\right)\right)\right)=branch))$$

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

Source. Repository-derived.

Commentary.

Here k=pathCost(r)+1. Guarded atomic navigation reaches beta from alpha and the pair (beta,alpha) from beta at that same literal address and count. The unconditional subtree/readout identity transfers these reached roots to the actual four-valued replies.

Theorem 1.2 (Whole-vector collision, rank separation and one legal future count).

$$\forall D:Nat,(\forall S:Menu,((\forall q:Address,((q\in S)⟹(\mathrm{length}\left(q\right)+1\le D)))⟹(\forall a,r:Address,(((r\ne \mathrm{nil}\left(\right))\wedge (\mathrm{append}\left(a,r\right)\in S)\wedge (\neg (a\in S)))⟹((2\le D)\wedge (\mathrm{height}\left(\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right)\right)=\mathrm{length}\left(a\right))\wedge (\mathrm{height}\left(\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right)\right)=\mathrm{length}\left(a\right))\wedge (\mathrm{length}\left(a\right)\le \mathrm{sub}\left(D,2\right))\wedge (\mathrm{Family}\left(D,\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right)\right)\right))\wedge (\mathrm{Family}\left(D,\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right)\right)\right))\wedge (\mathrm{initial}\left(S,\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right)\right)=\mathrm{initial}\left(S,\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right)\right))\wedge (\mathrm{initial}\left(\mathrm{publicMenu}\left(S\right),\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right)\right)\right)=\mathrm{initial}\left(\mathrm{publicMenu}\left(S\right),\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right)\right)\right))\wedge (\mathrm{code}\left(S,\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right)\right)\ne \mathrm{code}\left(S,\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right)\right))\wedge (\mathrm{pathCost}\left(r\right)+1<2\times D)\wedge (\mathrm{readout}\left(\mathrm{cons}\left(true,\mathrm{append}\left(a,r\right)\right),\mathrm{iterate}\left(substitution,\mathrm{pathCost}\left(r\right)+1,\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right)\right)\right)\right)=beta)\wedge (\mathrm{readout}\left(\mathrm{cons}\left(true,\mathrm{append}\left(a,r\right)\right),\mathrm{iterate}\left(substitution,\mathrm{pathCost}\left(r\right)+1,\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right)\right)\right)\right)=branch)\wedge (\mathrm{future}\left(S,\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right),\mathrm{pathCost}\left(r\right)+1\right)\ne \mathrm{future}\left(S,\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right),\mathrm{pathCost}\left(r\right)+1\right))\wedge (\mathrm{future}\left(\mathrm{publicMenu}\left(S\right),\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(true\right)\right)\right),\mathrm{pathCost}\left(r\right)+1\right)\ne \mathrm{future}\left(\mathrm{publicMenu}\left(S\right),\mathrm{outer}\left(\mathrm{spine}\left(a,\mathrm{of}\left(false\right)\right)\right),\mathrm{pathCost}\left(r\right)+1\right)))))))$$

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

Source. Repository-derived.

Commentary.

These conclusions all concern the same actual pair and the same supplied count. Each history uses its own fixed original source and genuine repeated substitution. Code inequality uses the original branch-first ranks of this pair, including the eta=0 overlap case. No generic quotient, coordinate-specific source choices or resource-efficiency assertion enters the result.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteMenuObstruction.atomic_separator
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteMenuObstruction.every_missing_prefix_obstruction
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeAlphaSpineObservation
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeDepthPatterns
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteMenuReconstruction
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeRankedNavigationCompiler