phi_inv
plain-language theorem explainer
Defines the reciprocal of the golden ratio as the steady-state active fraction in a Fibonacci recurrence model of lexicon evolution. Mathematical linguists or cognitive modelers tracking vocabulary acquisition would cite it for linking recognition cost fixed points to observed active-passive splits. The definition is a direct alias to the imported constant with no computation or lemmas.
Claim. Let $φ = (1 + √5)/2$ denote the golden ratio. Define $φ^{-1} := 1/φ$ as the predicted steady-state active-vocabulary fraction satisfying the fixed-point equation $x + x^2 = 1$.
background
The LexiconRatio module models lexicon growth via a two-state recurrence: active tokens at step n+1 equal the sum of prior active and passive tokens, while passive tokens at n+1 equal prior active tokens. This is the Fibonacci recurrence, so total lexicon size grows asymptotically as φ^n. The active fraction converges to the unique positive fixed point 1/φ of the ratio equation derived from the recurrence and the identity φ² = φ + 1. Upstream results establish the algebraic identity 1/φ = φ - 1 in Foundation.PhiForcing.phi_inv and Inequalities.phi_inv, quoting the doc-comment: 'φ^{-1} = φ - 1 (a key identity)'.
proof idea
One-line definition that directly aliases the golden ratio reciprocal from the Constants module. No tactics, reductions, or lemmas are invoked beyond the import of Constants.phi.
why it matters
Supplies the active fraction that feeds the downstream theorem fractions_sum_to_one proving phi_inv + passive_fraction = 1, realizing σ-conservation on the lexicon. It instantiates the T6 self-similar fixed point and T7 eight-tick octave structure from the forcing chain, replacing the v4 skeleton with a derivation from the recognition cost. The module doc-comment notes it is the unique positive solution of x + x² = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.