lexicon_ratio
plain-language theorem explainer
lexicon_ratio is defined as the inverse of the golden ratio, serving as the steady-state active fraction in a lexicon that evolves by the Fibonacci recurrence a_{n+1}=a_n+p_n, p_{n+1}=a_n. Cognitive scientists or linguists modeling vocabulary growth under σ-conservation would cite it as the unique positive solution to r + r² = 1. The definition is a direct one-line alias to phi_inv, inheriting the fixed-point identity from φ² = φ + 1.
Claim. The active fraction of the lexicon is the real number r = φ^{-1}, where φ = (1 + √5)/2 satisfies φ² = φ + 1 and r is the unique positive solution of r + r² = 1.
background
The module models a lexicon with active tokens a_n and passive tokens p_n that obeys the σ-conserving recurrence a_{n+1} = a_n + p_n, p_{n+1} = a_n derived from the active-edge budget. Total size L_n grows as φ^n, so the active fraction r = a_n/L_n converges to the fixed point of the recurrence. Upstream results establish that phi_inv equals 1/Constants.phi and satisfies the identity φ^{-1} = φ - 1 via the equation φ² = φ + 1.
proof idea
One-line definition that directly aliases lexicon_ratio to the sibling definition phi_inv (itself 1/Constants.phi). No tactics or lemmas are applied inside the body; all properties are inherited from the upstream phi_inv theorems.
why it matters
This definition supplies the core quantity for the downstream LexiconRatioCert structure and the theorems lexicon_ratio_derivation, lexicon_ratio_one_statement, and lexicon_ratio_band. It realizes the Fibonacci fixed point forced by the recognition cost identity φ² = φ + 1, closing the derivation that replaces the v4 literal assignment. It sits inside the self-similar fixed-point step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.