lexicon_ratio_band
plain-language theorem explainer
Lexicon ratio, the limiting active fraction in a Fibonacci-evolving lexicon under σ-conservation, satisfies 0.6 < ratio < 0.7. Recognition theorists deriving linguistic statistics from J-cost minima or linguists modeling token recruitment cite this interval. The proof is a one-line term that reuses the already-established band for the inverse golden ratio after definitional unfolding.
Claim. Let $r$ denote the lexicon ratio, the limiting active fraction $a_n/L_n$ in the Fibonacci recurrence model. Then $0.6 < r < 0.7$.
background
The LexiconRatio module models a lexicon with active tokens $a_{n+1}=a_n+p_n$ and passive tokens $p_{n+1}=a_n$, the Fibonacci recurrence forced by σ-conservation from the active-edge budget. Total size grows asymptotically as $L_n∼φ^n$, so the active fraction converges to the fixed point $1/φ$. The definition sets lexicon_ratio to phi_inv, the inverse golden ratio. Upstream, ObserverForcing.identity places the J-cost minimum at state 1, while PrimitiveDistinction.from supplies the structural axioms. The numerical band for phi_inv is already proved in phi_inv_band using Constants bounds on φ.
proof idea
The proof is a term-mode one-liner consisting of the identifier phi_inv_band. Once the type checker unfolds the definition lexicon_ratio := phi_inv, the goal reduces directly to the phi_inv band statement.
why it matters
This bound supplies the interval component of lexiconRatioCert, which assembles positivity, the band, the Fibonacci identity phi_inv + phi_inv² = 1, and the phi² identity. It certifies that the fixed point forced by the recognition cost equation and σ-conservation lies in the observed linguistic range, closing the derivation that replaces earlier skeleton definitions. The result sits inside the phi-ladder lattice and links to the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.