lexicon_ratio_one_statement
plain-language theorem explainer
The theorem packages three identities: the lexicon active fraction r satisfies the fixed-point equation r + r² = 1, the golden ratio obeys φ² = φ + 1, and active plus passive fractions sum to one. Researchers deriving linguistic statistics from recognition-cost conservation or modeling lexical evolution via Fibonacci recurrences would cite this result. The proof is a direct term that assembles the conjunction from the fixed-point lemma, the quadratic identity, and the σ-conservation sum.
Claim. Let $r$ be the active lexicon fraction and $p$ the passive fraction. Then $r + r^2 = 1$, $φ^2 = φ + 1$, and $r + p = 1$.
background
The module models a lexicon with two states evolving under σ-conservation: one new token per tick with active tokens at step n+1 equal to the sum of active and passive at n, and passive at n+1 equal to active at n. This produces the Fibonacci recurrence whose steady-state ratio converges to the unique positive solution of x + x² = 1. The active fraction is defined as phi_inv (i.e., 1/φ) and the passive fraction as 1 - phi_inv. Upstream, Constants bundles the CPM parameters whose σ-conservation forces the quadratic identity φ² = φ + 1. The doc-comment states that the active fraction is derived as the unique positive fixed point of the Fibonacci recurrence x + x² = 1 and that active + passive = 1 is σ-conservation.
proof idea
The proof is a term-mode one-liner that constructs the conjunction directly from three prior results: lexicon_ratio_derivation supplies the fixed-point identity, phi_sq supplies the quadratic relation for φ, and fractions_sum_to_one supplies the sum of active and passive fractions to unity.
why it matters
This bundles the algebraic core that links the lexicon model to the same φ forced as the self-similar fixed point in the recognition framework (T6). It replaces an earlier asserted definition with a derivation from σ-conservation on the recognition cost, closing the step that sets the active fraction to 1/φ. The result sits inside the broader forcing chain that produces D = 3 and the alpha band; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.