phi_sq
plain-language theorem explainer
The golden ratio satisfies φ² = φ + 1. Lexicon evolution models cite this identity to obtain the steady-state active fraction 1/φ from the Fibonacci recurrence on active and passive token counts. The proof is a direct one-line reference to the algebraic lemma that establishes the identity from the quadratic x² - x - 1 = 0.
Claim. Let φ be the golden ratio. Then φ² = φ + 1.
background
The LexiconRatio module models a lexicon with a_n active tokens and p_n passive tokens obeying the σ-conserving recurrence a_{n+1} = a_n + p_n, p_{n+1} = a_n. This is the Fibonacci recurrence whose total size L_n grows asymptotically as φ^n; the active fraction a_n/L_n converges to the fixed point 1/φ. The identity φ² = φ + 1 is imported from Constants.phi_sq_eq, whose doc-comment states it is the key identity from the defining equation x² - x - 1 = 0.
proof idea
The proof is a one-line wrapper that applies the lemma Constants.phi_sq_eq.
why it matters
This identity supplies the algebraic step needed to show that the passive fraction equals 1/φ² and that 1/φ + 1/φ² = 1, closing the σ-conservation condition for the lexicon steady state. It feeds the sibling derivations of phi_inv and passive_fraction_eq_phi_sq_inv inside the same module and aligns with the self-similar fixed-point forcing (T6) in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.