Native Ancestor Area Choices

Abstract

Independent bracket choices in a native Fibonacci source preserve the leaf word and have an exact affine ancestor-area formula.

Sources are nonempty ordered binary trees with beta and alpha leaves. The canonical source T at generation n is the n-fold Fibonacci substitution of alpha. The left-associated source B and the right-associated source D both have leaf word beta, alpha, beta.

Definition 1.1 (The canonical three-leaf source).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.defectB

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.defectB (✓ std3).

Source. Repository-derived.

Commentary.

B is pair(pair(beta,alpha),beta).

Definition 1.2 (The bracket defect).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.defectD

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.defectD (✓ std3).

Source. Repository-derived.

Commentary.

D is pair(beta,pair(alpha,beta)).

Definition 1.3 (All literal three-leaf positions).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.positions

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.positions (✓ std3).

Source. Repository-derived.

Commentary.

positions(t) consists of every actual address whose subtree in t is B.

Definition 1.4 (Simultaneous native choices).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.fill

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.fill (✓ std3).

Source. Repository-derived.

Commentary.

fill(t,a) replaces B by D precisely at the original positions where the Boolean choice a is true.

Definition 1.5 (The finite-subset family).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.variant

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.variant (✓ std3).

Source. Repository-derived.

Commentary.

variant(t,A) uses the membership indicator of A as the simultaneous choice.

Theorem 1.6 (The subtree at an original position).

$$\forall t:\mathrm{Source},(\forall a:\mathrm{Address}\to \mathrm{Bool},(\forall p:\mathrm{Address},((\mathrm{Member}\left(p,\mathrm{positions}\left(t\right)\right))⟹(\mathrm{subtree}\left(p,\mathrm{fill}\left(t,a\right)\right)=\mathrm{some}\left(\mathrm{ite}\left(a\left(p\right),\mathrm{defectD},\mathrm{defectB}\right)\right)))))$$

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

Source. Repository-derived.

Commentary.

Every original B position remains present after simultaneous filling. Its subtree is exactly D for a true choice and B for a false choice.

Definition 1.7 (Euclidean ancestor-area vector).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.areaVector

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.areaVector (✓ std3).

Source. Repository-derived.

Commentary.

areaVector(m,t) lists the products of the left and right child leaf counts in inorder gap order, in Euclidean space with m minus one coordinates. Unoccupied coordinates are zero.

Definition 1.8 (One unit of transferred area).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.gapVector

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.gapVector (✓ std3).

Source. Repository-derived.

Commentary.

gapVector(m,j) is the standard unit vector at j minus the standard unit vector at j plus one.

Definition 1.9 (The actual source family).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.sourceFamily

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.sourceFamily (✓ std3).

Source. Repository-derived.

Commentary.

sourceFamily(t) is the image of the full powerset of positions(t) under variant(t).

Definition 1.10 (The complete Euclidean vertex set).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.areaVertices

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.areaVertices (✓ std3).

Source. Repository-derived.

Commentary.

areaVertices(t) is the image of the same powerset under the ancestor-area vector.

Definition 1.11 (The normalized Euclidean family).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.normalizedAreaFamily

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.normalizedAreaFamily (✓ std3).

Source. Repository-derived.

Commentary.

The area vertices of T(n) are scaled by the reciprocal of choose(fib(n plus one),two).

Definition 1.12 (Normalized independent directions).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.unitDirection

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.unitDirection (✓ std3).

Source. Repository-derived.

Commentary.

Each signed gap vector is divided by square root two.

Definition 1.13 (The direction space).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.directionSpan

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.directionSpan (✓ std3).

Source. Repository-derived.

Commentary.

The real span of the normalized gap vectors is the Euclidean direction space of the cube.

Definition 1.14 (The cube in its own direction space).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.intrinsicCube

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.intrinsicCube (✓ std3).

Source. Repository-derived.

Commentary.

This is the inverse image of the convex hull under x maps to areaVector(t) plus x, with x in directionSpan(t). Its volume is the canonical Euclidean volume on that subspace.

Theorem 1.15 (The native family, area formula and squared distances).

$$\forall n:\mathbb{N},((3\le n)⟹((\mathrm{card}\left(\mathrm{positions}\left(T\left(n\right)\right)\right)=\mathrm{fib}\left(n-2\right))\wedge ((\mathrm{InjectiveOn}\left(\mathrm{variant}\left(T\left(n\right)\right),\mathrm{powerset}\left(\mathrm{positions}\left(T\left(n\right)\right)\right)\right))\wedge ((\forall A:\mathrm{Finset}\left(\mathrm{Address}\right),((\mathrm{Subset}\left(A,\mathrm{positions}\left(T\left(n\right)\right)\right))⟹((\mathrm{wd}\left(\mathrm{variant}\left(T\left(n\right),A\right)\right)=\mathrm{wd}\left(T\left(n\right)\right))\wedge ((\mathrm{length}\left(\mathrm{variant}\left(T\left(n\right),A\right)\right)=\mathrm{fib}\left(n+1\right))\wedge ((\mathrm{depth}\left(\mathrm{variant}\left(T\left(n\right),A\right)\right)=\mathrm{ite}\left(A=\varnothing ,n,0\right))\wedge ((\mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{variant}\left(T\left(n\right),A\right)\right)=\mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),T\left(n\right)\right)+\sum _{p\in A}\mathrm{gapVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{offset}\left(T\left(n\right),p\right)\right))\wedge ((\sum _{i:\mathrm{Fin}\left(\mathrm{fib}\left(n+1\right)-1\right)}\mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{variant}\left(T\left(n\right),A\right),i\right)=\mathrm{choose}\left(\mathrm{fib}\left(n+1\right),2\right))\wedge ((\mathrm{length}\left(\mathrm{coordinates}\left(\mathrm{variant}\left(T\left(n\right),A\right)\right)\right)=\mathrm{fib}\left(n+1\right)-1)\wedge (\forall B:\mathrm{Finset}\left(\mathrm{Address}\right),((\mathrm{Subset}\left(B,\mathrm{positions}\left(T\left(n\right)\right)\right))⟹(\mathrm{norm}{\left(\mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{variant}\left(T\left(n\right),A\right)\right)-\mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{variant}\left(T\left(n\right),B\right)\right)\right)}^2=2\times \mathrm{card}\left(\mathrm{symmDiff}\left(A,B\right)\right))))))))))))\wedge ((\forall p:\mathrm{Address},(\mathrm{Iff}\left(\mathrm{mem}\left(p,\mathrm{positions}\left(T\left(n\right)\right)\right),\mathrm{subtree}\left(p,T\left(n\right)\right)=\mathrm{some}\left(\mathrm{defectB}\right)\right)))\wedge ((\forall p:\mathrm{Address},((\mathrm{mem}\left(p,\mathrm{positions}\left(T\left(n\right)\right)\right))⟹((\mathrm{offset}\left(T\left(n\right),p\right)<\mathrm{fib}\left(n+1\right)-1)\wedge (\mathrm{offset}\left(T\left(n\right),p\right)+1<\mathrm{fib}\left(n+1\right)-1))))\wedge ((\forall p:\mathrm{Address},((\mathrm{mem}\left(p,\mathrm{positions}\left(T\left(n\right)\right)\right))⟹(\forall q:\mathrm{Address},((\mathrm{mem}\left(q,\mathrm{positions}\left(T\left(n\right)\right)\right))⟹((p\ne q)⟹((\mathrm{offset}\left(T\left(n\right),p\right)+3\le \mathrm{offset}\left(T\left(n\right),q\right))\vee (\mathrm{offset}\left(T\left(n\right),q\right)+3\le \mathrm{offset}\left(T\left(n\right),p\right))))))))\wedge ((\mathrm{convexHull}\left(\mathbb{R},\mathrm{areaVertices}\left(T\left(n\right)\right)\right)=\mathrm{singleton}\left(\mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),T\left(n\right)\right)\right)+\mathrm{parallelepiped}\left(p:\mathrm{positions}\left(T\left(n\right)\right)\mapsto \mathrm{gapVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{offset}\left(T\left(n\right),p\right)\right)\right))\wedge ((\mathrm{direction}\left(\mathrm{affineSpan}\left(\mathbb{R},\mathrm{convexHull}\left(\mathbb{R},\mathrm{areaVertices}\left(T\left(n\right)\right)\right)\right)\right)=\mathrm{directionSpan}\left(T\left(n\right)\right))\wedge ((\mathrm{Orthonormal}\left(\mathbb{R},\mathrm{unitDirection}\left(T\left(n\right)\right)\right))\wedge ((\mathrm{directionSpan}\left(T\left(n\right)\right)=\mathrm{span}\left(\mathbb{R},\mathrm{range}\left(p:\mathrm{positions}\left(T\left(n\right)\right)\mapsto \mathrm{gapVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{offset}\left(T\left(n\right),p\right)\right)\right)\right))\wedge ((\mathrm{finrank}\left(\mathbb{R},\mathrm{directionSpan}\left(T\left(n\right)\right)\right)=\mathrm{fib}\left(n-2\right))\wedge ((\forall p:\mathrm{positions}\left(T\left(n\right)\right),(\mathrm{norm}\left(\mathrm{gapVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{offset}\left(T\left(n\right),p\right)\right)\right)=\mathrm{sqrt}\left(2\right)))\wedge (\mathrm{volume}\left(\mathrm{intrinsicCube}\left(T\left(n\right)\right)\right)=\mathrm{ofReal}\left(2^{\frac{\mathrm{fib}\left(n-2\right)}{2}}\right)))))))))))))))$$

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

Source. Repository-derived.

Commentary.

For n at least three, all B positions are counted by fib(n minus two). Distinct subsets give distinct actual trees. Every choice preserves the leaf word and the fib(n plus one) leaf count. The empty subset has intrinsic substitution depth n, and every nonempty subset has depth zero.

Coordinates record the product of the two child leaf counts at each internal gap. Replacing B changes its two internal coordinates from [1,2] to [2,1]. An arbitrary context with equal-length fillings has the same exterior coordinate lists. Adding positions one at a time gives the stated sum of signed gap vectors. Distinct positions occupy disjoint gap pairs. Squared Euclidean distance is twice the cardinality of the symmetric difference of the choices, and total area is preserved.

The convex hull is the translate of the parallelepiped of the independent signed gap vectors: its coefficients range independently from zero to one. After division by square root two these vectors are orthonormal. Their direction span has dimension fib(n minus two), every edge has length square root two, and the canonical volume in that direction space is two to the power fib(n minus two) divided by two.

Theorem 1.16 (Exact normalized diameter and decay).

$$(\forall n:\mathbb{N},((3\le n)⟹((\mathrm{diam}\left(\mathrm{normalizedAreaFamily}\left(n\right)\right)=\frac{\mathrm{sqrt}\left(2\times \mathrm{fib}\left(n-2\right)\right)}{\mathrm{choose}\left(\mathrm{fib}\left(n+1\right),2\right)})\wedge ((\mathrm{card}\left(\mathrm{sourceFamily}\left(T\left(n\right)\right)\right)=2^{\mathrm{fib}\left(n-2\right)})\wedge (((\mathrm{depth}\left(\mathrm{variant}\left(T\left(n\right),\varnothing \right)\right)=n)\wedge (\mathrm{depth}\left(\mathrm{variant}\left(T\left(n\right),\mathrm{positions}\left(T\left(n\right)\right)\right)\right)=0))\wedge (\mathrm{norm}\left(\mathrm{choose}{\left(\mathrm{fib}\left(n+1\right),2\right)}^{-1}\times \mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{variant}\left(T\left(n\right),\varnothing \right)\right)-\mathrm{choose}{\left(\mathrm{fib}\left(n+1\right),2\right)}^{-1}\times \mathrm{areaVector}\left(\mathrm{fib}\left(n+1\right),\mathrm{variant}\left(T\left(n\right),\mathrm{positions}\left(T\left(n\right)\right)\right)\right)\right)=\mathrm{diam}\left(\mathrm{normalizedAreaFamily}\left(n\right)\right)))))))\wedge ((\mathrm{IsBigO}\left(\mathrm{atTop},n\mapsto \mathrm{diam}\left(\mathrm{normalizedAreaFamily}\left(n\right)\right),n\mapsto \mathrm{fib}{\left(n+1\right)}^{-\frac{3}{2}}\right))\wedge (\mathrm{Tendsto}\left(n\mapsto \mathrm{diam}\left(\mathrm{normalizedAreaFamily}\left(n\right)\right),\mathrm{atTop},\mathrm{nhds}\left(0\right)\right)))$$

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

Source. Repository-derived.

Commentary.

The empty and full subsets attain the maximal Euclidean separation. Scaling by the reciprocal total area gives the exact normalized diameter. There remain two to the power fib(n minus two) distinct sources, with depth n at the empty choice and zero at the full choice.

Writing M for fib(n plus one) and K for fib(n minus two), the inequalities K at most M and choose(M,two) at least M squared divided by four bound the diameter by four times square root two times M to the power minus three halves. Since the Fibonacci leaf count diverges, the diameter tends to zero.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.areaVector
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.areaVertices
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.defectB
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.defectD
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.directionSpan
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.fill
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.fill_at
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.gapVector
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.intrinsicCube
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.native_area_cube
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.normalizedAreaFamily
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.normalized_cube_diameter
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.positions
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.sourceFamily
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.unitDirection
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeAncestryDefectCube.variant
• Dependency: D5/S3/Arith/FibonacciAtomic/ActualHistorySingleHoleRecovery
• Dependency: D5/S3/Arith/FibonacciAtomic/ActualImageAlphaSeparation
• Dependency: D5/S3/Arith/FibonacciAtomic/ActualLeafHistoryRigidity
• Dependency: D5/S3/Arith/FibonacciAtomic/Geometry/AncestorAreaInterval
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/NativeRotationDepthGap