Sharp Entrance Ratios on Entire Actual Geometry Fibers

Abstract

Entire same-word geometry fibers include every ordered shape and every pure substitution entrance.

T is FreeMagma Bool. True is alpha and false is beta. Pairing retains both children in order. The substitution rho sends alpha to beta, beta to (beta,alpha), and a pair to the pair of substituted children. The word wd(t) lists every leaf of t from left to right. G is the five-coordinate endpoint, signed area and two centered moments of that same word, with unit steps (1,0) and (0,1). Its codomain Five is the original real coordinate structure; no separate coordinate representatives are chosen.

Definition 1.1 (Whole word fiber).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.WordFiber

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.WordFiber (✓ std3).

Source. Repository-derived.

Commentary.

WordFiber(g) is the subtype of all nonempty Boolean lists w with G(w)=g.

Definition 1.2 (Whole ordered tree fiber).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.TreeFiber

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.TreeFiber (✓ std3).

Source. Repository-derived.

Commentary.

TreeFiber(g) is the subtype of all actual trees t:T with G(wd(t))=g. Every ordered shape is included.

Definition 1.3 (All pure entrances).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.EntranceFiber

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.EntranceFiber (✓ std3).

Source. Repository-derived.

Commentary.

EntranceFiber(g) consists of all triples (y,x,k):T times T times Nat with G(wd(y))=g and rho^k(x)=y. All natural k are permitted.

Definition 1.4 (Actual leaf number).

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

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

Source. Repository-derived.

Commentary.

N(g) is the natural floor of g.u+g.v. On any nonempty actual fiber it equals the positive word and tree length.

Definition 1.5 (Forward geometry).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.L

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.L (✓ std3).

Source. Repository-derived.

Commentary.

L(u,v,d,e,f)=(v,u+v,-d-v,v-f,-v-3d-e-f).

Definition 1.6 (Inverse candidate).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.Linv

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.Linv (✓ std3).

Source. Repository-derived.

Commentary.

Linv(u,v,d,e,f)=(v-u,u,-d-u,u+3d+e-f,u-e). This is an inverse on the ambient coordinates; membership still requires an actual word or tree.

Definition 1.7 (Letter substitution).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.letter

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.letter (✓ std3).

Source. Repository-derived.

Commentary.

letter(true)=[false], and letter(false)=[false,true].

Definition 1.8 (Actual word substitution).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.sigma

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.sigma (✓ std3).

Source. Repository-derived.

Commentary.

sigma(w) is the concatenation of letter(c) for every letter occurrence c of w, in order.

Theorem 1.9 (Length on Every Actual Geometry Fiber).

$$\forall g:\mathrm{Five}\left(\right),(\forall t:\mathrm{TreeFiber}\left(g\right),(\mathrm{ell}\left(\mathrm{val}\left(t\right)\right)=N\left(g\right)))$$

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

Source. Repository-derived.

Commentary.

Every actual source in the entire geometry fiber has leaf count N(g). The statement includes every ordered shape and word with that exact G; an empty fiber has no members.

Theorem 1.10 (Exact Whole-Word Substitution).

$$\forall t:\mathrm{Source}\left(\right),(\mathrm{wd}\left(\mathrm{rho}\left(t\right)\right)=\mathrm{sigma}\left(\mathrm{wd}\left(t\right)\right))$$

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

Source. Repository-derived.

Commentary.

The literal ordered word of each substituted actual source is sigma of its complete original labelled word. Here ell is FreeMagma.length and Source is the actual FreeMagma Bool carrier.

Definition 1.11 (Word cardinality).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.m

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.m (✓ std3).

Source. Repository-derived.

Commentary.

m(g)=Nat.card(WordFiber(g)). The actual word carrier is proved finite before this definition.

Definition 1.12 (Tree cardinality).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.M

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.M (✓ std3).

Source. Repository-derived.

Commentary.

M(g)=Nat.card(TreeFiber(g)). The actual ordered tree carrier is proved finite before this definition.

Definition 1.13 (Entrance cardinality).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.H

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.H (✓ std3).

Source. Repository-derived.

Commentary.

H(g)=Nat.card(EntranceFiber(g)). Finiteness follows from a proved cutoff k<2N(g) for every legal entrance, together with finite current trees and finite possible source trees.

Definition 1.14 (Pure-word geometry).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.pure

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.pure (✓ std3).

Source. Repository-derived.

Commentary.

pure(true,n)=(n,0,0,0,0), and pure(false,n)=(0,n,0,0,0). These are exactly the geometries of the corresponding repeated-letter words.

Definition 1.15 (Sharp bound).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.B

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.B (✓ std3).

Source. Repository-derived.

Commentary.

B(n) is three at n=2, five halves at n=3, and two otherwise. In particular B(1)=2 and B(n)=2 for n>=4.

Definition 1.16 (Two-leaf maximizer).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.ba

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.ba (✓ std3).

Source. Repository-derived.

Commentary.

ba=(1,1,-1,1,-1) is the exact geometry of [false,true].

Definition 1.17 (Three-leaf maximizer).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.bab

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.bab (✓ std3).

Source. Repository-derived.

Commentary.

bab=(1,2,0,2,2) is the exact geometry of [false,true,false].

Definition 1.18 (Prefix odd moment).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.prefixMoment

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.prefixMoment (✓ std3).

Source. Repository-derived.

Commentary.

prefixMoment([])=0 and prefixMoment(a::l)=a+prefixMoment(l)+2 sum(l). For the reverse of the original descending rows, it is the sum of (2j-1)x(j) over the same word’s ascending prefix counts.

Definition 1.19 (Same-word arithmetic guards).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.SourceGuards

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.SourceGuards (✓ std3).

Source. Repository-derived.

Commentary.

SourceGuards(g) asserts one actual nonempty word w in WordFiber(g) and natural numbers k,q,t. They are, respectively, the sum of its original rows, the sum of the squared rows, and prefixMoment of the reverse rows. It includes k<=count(true,w) count(false,w), N(g)>0, g.u=count(true,w), g.v=count(false,w), and simultaneous integer d,e,f representing g.d,g.e,g.f. It also includes (g.d+g.u g.v)/2=k, (g.e+6g.u k-g.u^2 g.v)/6=q, and (g.f+6g.v k+g.u g.v^2)/6=t. Thus endpoints and all joint-moment guards belong to the same word, including pure words.

Definition 1.20 (Whole-fiber maximizer at every size).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.upper

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.upper (✓ std3).

Source. Repository-derived.

Commentary.

upper(n)=ba at n=2, bab at n=3, and pure(false,n) otherwise.

Theorem 1.21 (Actual Count Factorization and Recursion).

$$\forall g:\mathrm{Five}\left(\right),(((0<N\left(g\right))⟹(M\left(g\right)=\mathrm{Cat}\left(N\left(g\right)-1\right)\cdot m\left(g\right)))\wedge (H\left(g\right)=M\left(g\right)+H\left(\mathrm{Linv}\left(g\right)\right))\wedge (m\left(\mathrm{Linv}\left(g\right)\right)\le m\left(g\right))\wedge (M\left(g\right)\le H\left(g\right)))$$

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

Source. Repository-derived.

Commentary.

For every real candidate g, positive N gives the full ordered-shape factor Cat(N-1) times the whole word count. Independently of candidate validity, the all-entrance count splits into depth zero and the inverse candidate’s all-entrance count. Applying sigma injects that inverse candidate’s whole word fiber into the current one. Empty carriers contribute zero.

Theorem 1.22 (Uniform Bounds on Entire Actual Fibers).

$$\forall g:\mathrm{Five}\left(\right),((M\left(g\right)\le H\left(g\right))\wedge ((N\left(g\right)=1)⟹(H\left(g\right)\le 2\cdot M\left(g\right)))\wedge ((N\left(g\right)=2)⟹(H\left(g\right)\le 3\cdot M\left(g\right)))\wedge ((N\left(g\right)=3)⟹(2\cdot H\left(g\right)\le 5\cdot M\left(g\right)))\wedge ((4\le N\left(g\right))⟹(H\left(g\right)\le 2\cdot M\left(g\right)))\wedge (H\left(g\right)\le 3\cdot M\left(g\right)))$$

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

Source. Repository-derived.

Commentary.

The inequalities hold for all real candidates, hence for every nonempty actual geometry fiber. At one leaf the factor is two; at two leaves it is three; at three leaves the integer inequality 2H<=5M gives factor five halves; from four leaves onward the factor is two. The common factor three and the lower bound are included. These statements count all trees and all pure entrances; they impose no probability law on physical sources.

The induction uses literal entrance recursion and injection of actual whole word fibers. A pure beta fiber has the same leaf count as its pure alpha inverse and has twice its tree count in entrances. Every other nonempty inverse has fewer leaves. The two distinct endpoint terms of the nonnegative Catalan recurrence show that adjacent positive indices at least double, leaving only the one-, two- and three-leaf inverse cases for direct arithmetic comparison.

Theorem 1.23 (Complete Sharp Ratios and Full-Fiber Attainment).

$$(\forall g:\mathrm{Five}\left(\right),((\mathrm{Nonempty}\left(\mathrm{TreeFiber}\left(g\right)\right))⟹((\mathrm{SourceGuards}\left(g\right))\wedge (0<N\left(g\right))\wedge (0<M\left(g\right))\wedge (1\le \frac{H\left(g\right)}{M\left(g\right)})\wedge (\frac{H\left(g\right)}{M\left(g\right)}\le B\left(N\left(g\right)\right))\wedge (M\left(g\right)\le H\left(g\right))\wedge (H\left(g\right)\le 3\cdot M\left(g\right)))))\wedge (\forall n:\mathbb{N},((0<n)⟹((\mathrm{Nonempty}\left(\mathrm{TreeFiber}\left(\mathrm{pure}\left(true,n\right)\right)\right))\wedge (\mathrm{Nonempty}\left(\mathrm{TreeFiber}\left(\mathrm{pure}\left(false,n\right)\right)\right))\wedge (N\left(\mathrm{pure}\left(true,n\right)\right)=n)\wedge (N\left(\mathrm{pure}\left(false,n\right)\right)=n)\wedge (m\left(\mathrm{pure}\left(true,n\right)\right)=1)\wedge (m\left(\mathrm{pure}\left(false,n\right)\right)=1)\wedge (M\left(\mathrm{pure}\left(true,n\right)\right)=\mathrm{Cat}\left(n-1\right))\wedge (H\left(\mathrm{pure}\left(true,n\right)\right)=M\left(\mathrm{pure}\left(true,n\right)\right))\wedge (M\left(\mathrm{pure}\left(false,n\right)\right)=\mathrm{Cat}\left(n-1\right))\wedge (H\left(\mathrm{pure}\left(false,n\right)\right)=2\cdot M\left(\mathrm{pure}\left(false,n\right)\right))\wedge (\frac{H\left(\mathrm{pure}\left(true,n\right)\right)}{M\left(\mathrm{pure}\left(true,n\right)\right)}=1)\wedge (\frac{H\left(\mathrm{pure}\left(false,n\right)\right)}{M\left(\mathrm{pure}\left(false,n\right)\right)}=2)\wedge (\mathrm{Nonempty}\left(\mathrm{TreeFiber}\left(\mathrm{upper}\left(n\right)\right)\right))\wedge (N\left(\mathrm{upper}\left(n\right)\right)=n)\wedge (\frac{H\left(\mathrm{upper}\left(n\right)\right)}{M\left(\mathrm{upper}\left(n\right)\right)}=B\left(n\right)))))\wedge ((\mathrm{Nonempty}\left(\mathrm{TreeFiber}\left(\mathrm{ba}\left(\right)\right)\right))\wedge (N\left(\mathrm{ba}\left(\right)\right)=2)\wedge (\forall w:\mathrm{WordFiber}\left(\mathrm{ba}\left(\right)\right),(\mathrm{val}\left(w\right)=[false,true]))\wedge (m\left(\mathrm{ba}\left(\right)\right)=1)\wedge (M\left(\mathrm{ba}\left(\right)\right)=1)\wedge (H\left(\mathrm{ba}\left(\right)\right)=3)\wedge (\mathrm{Nonempty}\left(\mathrm{TreeFiber}\left(\mathrm{bab}\left(\right)\right)\right))\wedge (N\left(\mathrm{bab}\left(\right)\right)=3)\wedge (\forall w:\mathrm{WordFiber}\left(\mathrm{bab}\left(\right)\right),(\mathrm{val}\left(w\right)=[false,true,false]))\wedge (m\left(\mathrm{bab}\left(\right)\right)=1)\wedge (M\left(\mathrm{bab}\left(\right)\right)=2)\wedge (H\left(\mathrm{bab}\left(\right)\right)=5))\wedge (\forall c:\mathbb{R},((\forall g:\mathrm{Five}\left(\right),((\mathrm{Nonempty}\left(\mathrm{TreeFiber}\left(g\right)\right))⟹(\frac{H\left(g\right)}{M\left(g\right)}\le c)))⟹(3\le c)))$$

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

Source. Repository-derived.

Commentary.

Every nonempty actual tree fiber supplies the same-word arithmetic guards, positive leaf and tree counts, the exact ratio bounds, and M<=H<=3M. No additional guard hypothesis is imposed on actual trees. The proof of the upper bound uses the entire inverse word fiber and every inverse tree entrance.

At each positive n, the complete pure alpha and pure beta fibers each have one leaf word and Cat(n-1) ordered shapes. Their entrance ratios are one and two. The whole fiber at upper(n) attains B(n). At ba the unique word is beta alpha, with M=1 and H=3; at bab the unique word is beta alpha beta, with M=2 and H=5. The inverse chain bab, ba, beta, alpha counts all entrances by the proved recursion, including the primitive three-leaf shape. Consequently every uniform real upper bound on the ratios is at least three.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.B
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.EntranceFiber
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.H
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.L
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.Linv
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.M
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.N
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.SourceGuards
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.TreeFiber
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.WordFiber
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.actual_fiber_counting
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.ba
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.bab
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.letter
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.m
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.prefixMoment
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.pure
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.sharp_geometry_entrance_ratio
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.sigma
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.tree_length
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.uniform_actual_entrance_estimate
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.upper
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/GeometryEntranceRatio.wd_substitution
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceTransportCentralizer
• Dependency: D5/S3/Combinatorics/Partitions/WordPartitionInverse