lexicon_ratio_derivation
plain-language theorem explainer
The lexicon active fraction r satisfies the quadratic r + r² = 1, which is the steady-state condition for the two-state Fibonacci recurrence on active and passive tokens. Recognition theorists modeling language evolution would cite this to obtain the active/passive split directly from the golden-ratio fixed point. The proof is a one-line term application of the phi inverse Fibonacci fixed point lemma.
Claim. Let $r$ be the steady-state active fraction of the lexicon in the two-state model. Then $r + r^2 = 1$.
background
The module models lexicon evolution over discrete ticks with active tokens $a_n$ and passive tokens $p_n$ obeying the recurrence $a_{n+1} = a_n + p_n$, $p_{n+1} = a_n$. This is the Fibonacci recurrence; total size $L_n$ grows asymptotically as $L_n ∼ φ^n$. The active fraction $r = a_n/L_n$ converges to the unique positive fixed point of the associated quadratic. The upstream lemma Constants.phi_sq_eq states φ² = φ + 1 and supplies the algebraic identity that converts the fixed-point equation into r + r² = 1.
proof idea
This is a one-line term-mode proof that directly invokes the phi_inv_fibonacci_fixed_point lemma (itself resting on phi_sq_eq). No additional tactics are required; the lemma already encodes the fixed-point solution for the inverse golden ratio under the quadratic derived from φ² = φ + 1.
why it matters
The result supplies the fibonacci_identity clause inside lexiconRatioCert and is one conjunct of lexicon_ratio_one_statement, which bundles the ratio identity with phi_sq_eq and the partition into active plus passive fractions. It realizes the self-similar fixed point (T6) inside the linguistics track by deriving the active fraction from σ-conservation on the recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.