lexicon_ratio_pos
plain-language theorem explainer
Establishes that the lexicon ratio, the steady-state active fraction 1/phi in the two-state Fibonacci token recurrence, is strictly positive. Recognition theorists applying the phi fixed point to language dynamics cite it to anchor the active component above zero. The proof is a direct one-line reference to the positivity of 1/phi from the phi emergence foundation.
Claim. $0 < r$ where $r = 1/phi$ denotes the active fraction in the lexicon recurrence with $a_{n+1} = a_n + p_n$ and $p_{n+1} = a_n$.
background
The module models lexicon evolution via a sigma-conserving Fibonacci recurrence on active and passive token counts, with total size growing as phi^n. The active fraction converges to the fixed point 1/phi satisfying r + r^2 = 1. Upstream, phi_inv_pos from PhiEmergence states that 1/phi > 0, proved by one_div_pos.mpr phi_pos. The local definition sets lexicon_ratio to phi_inv.
proof idea
One-line wrapper that applies phi_inv_pos from the phi emergence module directly to the definition lexicon_ratio := phi_inv.
why it matters
Supplies the positivity component inside lexiconRatioCert, which bundles all ratio properties including the Fibonacci identity. It links the linguistic model to the phi self-similar fixed point and the eight-tick octave structure in the recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.