Whole guarded five-hole fibers and complete labels

Abstract

NativeFiveHoleFiber

Definition 1.1 (The complete guarded raw record).

$$\forall u:Source,((\mathrm{Raw}\left(u\right))⟺((\mathrm{literalRecord}\left(\mathrm{singleton}\left(\mathrm{nil}\left(\right)\right),u\right)=\mathrm{rootLabel}\left(\right))\wedge ((\mathrm{readout}\left(\mathrm{nil}\left(\right),u\right)=\mathrm{branch}\left(\right))\wedge ((\mathrm{readout}\left(R\left(\right),u\right)=\mathrm{branch}\left(\right))\wedge ((\mathrm{readout}\left(\mathrm{RR}\left(\right),u\right)=\mathrm{branch}\left(\right))\wedge ((\mathrm{readout}\left(\mathrm{RRR}\left(\right),u\right)=\mathrm{branch}\left(\right))\wedge ((\mathrm{readout}\left(\mathrm{RRRLL}\left(\right),u\right)=\mathrm{alpha}\left(\right))\wedge ((\mathrm{readout}\left(\mathrm{RRRRL}\left(\right),u\right)=\mathrm{alpha}\left(\right))\wedge ((\mathrm{GuardedEqual}\left(0,\mathrm{RRRLR}\left(\right),1,\mathrm{RL}\left(\right),u\right))\wedge (\mathrm{GuardedEqual}\left(0,\mathrm{RRRRR}\left(\right),1,\mathrm{RRL}\left(\right),u\right)))))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.Raw (✓ std3).

Source. Repository-derived.

Commentary.

Source is the finite free magma on the two native leaves. Addresses are Boolean words, false for L and true for R. F(y) pairs alpha with the actual substitution of y. V(x,y,z) pairs x with the successive holes y, z, F(y), F(z). Q consists of L, RL, RRL, RRRL and RRRR.

RootLabel is the complete one-hole row at the empty address. GuardedEqual requires presence at both supplied endpoints and equality of the entire transformed subtrees. All original literals and both positive copies concern the same finite source.

Theorem 1.2 (The complete root row is constant).

$$\forall u:Source,(\mathrm{literalRecord}\left(\mathrm{singleton}\left(\mathrm{nil}\left(\right)\right),u\right)=\mathrm{rootLabel}\left(\right))$$

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

Source. Repository-derived.

Commentary.

Every nonempty finite source is hidden by the root hole. Its literal exterior is the empty-address hole and its complete partition has one class. This equality keeps the entire row, including the partition, rather than only a point reply.

Theorem 1.3 (Every raw source has the full source shape).

$$\forall u:Source,((\mathrm{Raw}\left(u\right))⟺(\exists x,y,z:Source,(u=V\left(x,y,z\right))))$$

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

Source. Repository-derived.

Commentary.

The four branch replies extract the full outer skeleton. The alpha replies force branches in its last two holes. Transport at epoch one and the guarded copies identify their right children with the substitutions of y and z. Conversely every source of this shape satisfies the root row, every literal, both endpoint guards and both copied equalities. The parameterization covers the entire raw fiber.

Theorem 1.4 (All cut endpoints remain reached at every epoch).

$$\forall a:Nat,(\forall x,y,z:Source,(\forall i:\mathrm{Fin}\left(5\right),(\mathrm{subtree}\left(\mathrm{position}\left(i\right),\mathrm{iterate}\left(\mathrm{substitution}\left(\right),a,V\left(x,y,z\right)\right)\right)=\mathrm{some}\left(\mathrm{iterate}\left(\mathrm{substitution}\left(\right),a,\mathrm{hole}\left(x,y,z,i\right)\right)\right))))$$

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

Source. Repository-derived.

Commentary.

Original present transport applies at each already reached cut address. Arbitrary supplied natural epochs retain both guards of every negative record. The comparison is between entire transformed holes.

Definition 1.5 (All six class comparisons).

$$\forall y,z:Source,((\mathrm{Distinct}\left(y,z\right))⟺((y\ne z)\wedge ((y\ne F\left(y\right))\wedge ((y\ne F\left(z\right))\wedge ((z\ne F\left(y\right))\wedge ((z\ne F\left(z\right))\wedge (F\left(y\right)\ne F\left(z\right))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.Distinct (✓ std3).

Source. Repository-derived.

Commentary.

Both labels contain the same complete four-branch exterior. The false label has partition blocks {L,RL}, {RRL}, {RRRL}, {RRRR}. The true label has blocks {L,RRRL}, {RL}, {RRL}, {RRRR}. Label compares every ordered pair in Q, including reflexive and reversed pairs.

Theorem 1.6 (The entire exterior and partition determine the parameters).

$$\forall s:Bool,(\forall x,y,z:Source,((\mathrm{literalRecord}\left(Q\left(\right),V\left(x,y,z\right)\right)=\mathrm{label}\left(s\right))⟺((x=\mathrm{ite}\left(s,F\left(y\right),y\right))\wedge (\mathrm{Distinct}\left(y,z\right)))))$$

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

Source. Repository-derived.

Commentary.

The forward direction extracts the repeated block and all six inequalities from the complete partition. The reverse checks every pair of holes and the whole exterior. No chosen representative narrows the fiber.

Theorem 1.7 (Exact membership in each original whole stratum).

$$\forall s:Bool,(\forall H:History,(\forall u:Source,((\mathrm{Stratum}\left(s,H,u\right))⟺(\exists y,z:Source,((u=\mathrm{source}\left(s,y,z\right))\wedge ((\mathrm{Distinct}\left(y,z\right))\wedge (\mathrm{Protected}\left(H,\mathrm{source}\left(s,y,z\right)\right))))))))$$

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

Source. Repository-derived.

Commentary.

History is any finite list of negative records between Q endpoints, at arbitrary supplied natural epochs. Supported constrains only endpoints. IndexedHistory reconstructs the original list exactly, retaining order and repetitions. Negative contains both guards and the whole-subtree disequality. Protected conjoins every original occurrence. D is Raw intersected with Protected; Stratum additionally fixes the full literal record. Other labels of D remain part of D.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.Distinct
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.Raw
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.complete_label_iff
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.epoch_hole
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.raw_fiber_iff
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.raw_stratum_iff
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiveHoleFiber.root_record
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeDepthPatterns