Actual Fibonacci Descendant Masses

Abstract

Original guarded address geometry and uniform all-occurrence cylinder masses.

Definition 1.1 (vertices).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.vertices

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.vertices (✓ std3).

Source. Repository-derived.

Commentary.

vertices(n) contains every original occurrence address of T(n), with the root included.

Definition 1.2 (N).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.N

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.N (✓ std3).

Source. Repository-derived.

Commentary.

N(n) is the cardinality of vertices(n).

Definition 1.3 (Node).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.Node

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.Node (✓ std3).

Source. Repository-derived.

Commentary.

Node(n) is the subtype of actual occurrence addresses of T(n).

Definition 1.4 (μ).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.μ

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.μ (✓ std3).

Source. Repository-derived.

Commentary.

mu(n) is the uniform probability measure on Node(n); it assigns equal mass to roots, branches and both terminal labels.

Definition 1.5 (descendants).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.descendants

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.descendants (✓ std3).

Source. Repository-derived.

Commentary.

descendants(n,p) filters vertices(n) by the original prefix relation.

Definition 1.6 (mass).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.mass

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.mass (✓ std3).

Source. Repository-derived.

Commentary.

mass(n,p) is the cardinality of descendants(n,p) divided by N(n).

Definition 1.7 (a).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.a

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.a (✓ std3).

Source. Repository-derived.

Commentary.

a is the reciprocal of the real golden ratio.

Theorem 1.8 (All Occurrence Cardinality).

$$\forall n:\mathbb{N},(N\left(n\right)=((2)\cdot (\mathrm{fib}\left((n)+(1)\right)))-(1))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.cardinality (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every original finite source has twice its Fibonacci leaf count minus one occurrences. The subtraction is in the natural numbers, including the singleton sources.

Theorem 1.9 (Occurrence and Subtree).

$$\forall S:\mathrm{Source}\left(\right),(\forall x:\mathrm{Address}\left(\right),((x\in \mathrm{nodes}\left(S\right))⟺(\exists U:\mathrm{Source}\left(\right),(\mathrm{subtree}\left(x,S\right)=\mathrm{some}\left(U\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.node_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

An address occurs in an arbitrary original source exactly when its addressed subtree exists.

Theorem 1.10 (Actual Fibonacci Descendant Masses).

$$((((((((\forall n:\mathbb{N},(\forall p:\mathrm{Address}\left(\right),((p\ne [])⟹((\exists U:\mathrm{Source}\left(\right),(\mathrm{subtree}\left(p,T\left(n\right)\right)=\mathrm{some}\left(U\right)))⟺((\mathrm{pathCost}\left(p\right)\le n)\wedge ((\mathrm{pathCost}\left(\mathrm{dropLast}\left(p\right)\right))+(2)\le n))))))\wedge (\forall n:\mathbb{N},(\forall p:\mathrm{Address}\left(\right),((p\ne [])⟹((\mathrm{pathCost}\left(p\right)\le n)⟹(((\mathrm{pathCost}\left(\mathrm{dropLast}\left(p\right)\right))+(2)\le n)⟹((\mathrm{subtree}\left(p,T\left(n\right)\right)=\mathrm{some}\left(T\left((n)-(\mathrm{pathCost}\left(p\right))\right)\right))\wedge (\mathrm{mass}\left(n,p\right)=\frac{N\left((n)-(\mathrm{pathCost}\left(p\right))\right)}{N\left(n\right)}))))))))\wedge (\forall n:\mathbb{N},(\forall p:\mathrm{Address}\left(\right),((\mathrm{subtree}\left(p,T\left(n\right)\right)=\mathrm{none}\left(\right))⟹(\mathrm{mass}\left(n,p\right)=0)))))\wedge (\forall n:\mathbb{N},(\forall p:\mathrm{Address}\left(\right),(\mathrm{mass}\left(n,p\right)\le ((2)\cdot (\mathrm{goldenRatio}\left(\right)))\cdot ((a{)}^{\mathrm{length}\left(p\right)})))))\wedge (\forall n:\mathbb{N},(\forall p:\mathrm{Address}\left(\right),(\mathrm{descendantMeasure}\left(n,p\right)=\mathrm{mass}\left(n,p\right)))))\wedge (\forall n:\mathbb{N},(\forall x:\mathrm{Node}\left(n\right),(\mathrm{pointMeasure}\left(n,x\right)=\frac{1}{N\left(n\right)}))))\wedge (\forall n:\mathbb{N},(\forall p:\mathrm{Address}\left(\right),((\mathrm{subtree}\left(p,T\left(n\right)\right)=\mathrm{some}\left(T\left((n)-(\mathrm{pathCost}\left(p\right))\right)\right))⟹(\mathrm{readout}\left(p,T\left(n\right)\right)=\mathrm{label}\left((n)-(\mathrm{pathCost}\left(p\right))\right))))))\wedge (\forall n:\mathbb{N},(\forall p:\mathrm{Address}\left(\right),(\forall b:\mathrm{Bool}\left(\right),((\mathrm{subtree}\left(p,T\left(n\right)\right)=\mathrm{some}\left(\mathrm{of}\left(b\right)\right))⟹(\forall q:\mathrm{Address}\left(\right),((q\ne [])⟹(\mathrm{subtree}\left(\mathrm{append}\left(p,q\right),T\left(n\right)\right)=\mathrm{none}\left(\right)))))))))\wedge (\forall n:\mathbb{N},((\mathrm{mass}\left(n,[]\right)=1)\wedge (\mathrm{readout}\left([],T\left(n\right)\right)=\mathrm{label}\left(n\right))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.finite_source_masses (✓ std3). ∎

Source. Repository-derived.

Commentary.

False denotes a left edge and true denotes a right edge. The inherited pathCost adds one for left and two for right. dropLast removes the final edge. A descent is permitted only from a branch, so both the final cost and the last-parent cost plus two must be at most n.

In the formula, label(d) is alpha for d=0, beta for d=1 and branch for d>=2. descendantMeasure(n,p) denotes the real value of mu(n) on the actual nodes whose addresses extend p. pointMeasure(n,x) is the extended nonnegative point mass of x. These quantities use all occurrences, including internal nodes and the root.

The guarded native navigation identifies the entire residual source at each reached address. Prefixing its node enumeration gives the actual ambient descendant set. The original node count is twice the Fibonacci leaf count minus one. Its recurrence yields golden-ratio upper and lower bounds, and their ratio gives the uniform envelope. An absent prefix has no descendants. A terminal cannot be crossed by a further nonempty suffix.

The two singleton sources are retained: the root is alpha at n=0 and beta at n=1. Both have total mass one.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.N
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.Node
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.a
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.cardinality
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.descendants
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.finite_source_masses
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.mass
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.node_iff
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.vertices
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/FiniteSourceMass.μ
• Dependency: D5/S0/Diagonal/Probability/EquivariantEscape
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/ActualCompletionHorizon
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeRankedNavigationCompiler
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap