phi_inv_fibonacci_fixed_point
plain-language theorem explainer
The inverse of the golden ratio satisfies x + x² = 1. This is the conservation identity for the steady-state active fraction in a two-state lexicon whose size evolves by the Fibonacci recurrence a_{n+1} = a_n + p_n, p_{n+1} = a_n. Recognition theorists deriving linguistic ratios from cost functions and linguists modeling lexical growth cite the result. The proof is a short algebraic reduction that invokes the defining relation φ² = φ + 1, clears denominators by field simplification, and closes by linear arithmetic.
Claim. Let φ denote the golden ratio. Then φ^{-1} + (φ^{-1})^2 = 1.
background
The module models a lexicon with active tokens a_n and passive tokens p_n obeying the σ-conserving recurrence a_{n+1} = a_n + p_n, p_{n+1} = a_n (one new token per tick from the active-edge budget). Total size L_n satisfies L_{n+1} = L_n + a_n and grows as L_n ∼ φ^n. The active fraction r = a_n / L_n converges to the fixed point of the recurrence, which is 1/φ. This fixed point obeys the identity r + r² = 1, obtained directly from the recognition-cost relation φ² = φ + 1. Upstream results supply φ^{-1} = φ - 1 and the square identity φ² = φ + 1.
proof idea
Unfold phi_inv to substitute the explicit expression in φ. Invoke positivity of φ to obtain a non-zero denominator. Apply the square identity phi_sq. Rewrite using div_pow and one_pow, then normalize with field_simp. Close the resulting polynomial equation by linarith using the square relation.
why it matters
The result is invoked verbatim by lexicon_ratio_derivation to certify the Fibonacci identity for the lexicon ratio, and it supports both passive_fraction_eq_phi_sq_inv and phi_inv_unique. It supplies the σ-conservation condition on the lexicon steady state required by the module's Fibonacci model. The identity instantiates the phi fixed-point property (T6) from the forcing chain inside a linguistic derivation, completing the active/passive fraction calculation without additional scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.