fractions_sum_to_one
plain-language theorem explainer
The active lexicon fraction 1/φ and passive fraction 1/φ² sum to one, confirming normalization in the steady-state model. Linguists or recognition theorists modeling vocabulary dynamics via Fibonacci recurrences would cite it as the σ-conservation identity. The proof is a one-line algebraic reduction after unfolding the passive fraction definition.
Claim. The active fraction $1/φ$ plus the passive fraction $1/φ^2$ equals 1.
background
The LexiconRatio module models lexicon evolution on a two-state system with a Fibonacci recurrence: active tokens at step n recruit one new active token from the passive pool while each active token becomes passive next. Total size grows asymptotically as φ^n. The active fraction is defined as 1/φ (the unique positive fixed point of x + x² = 1). The passive fraction is defined directly as 1 minus the active fraction, equivalently 1/φ².
proof idea
The proof is a one-line wrapper. It unfolds the definition of passive_fraction (which is 1 - phi_inv) and applies the ring tactic to reduce the identity using the algebraic properties of φ.
why it matters
This theorem is invoked inside lexicon_ratio_one_statement to bundle the fixed-point equation, the φ² = φ + 1 identity from Constants, and the sum-to-one normalization. It completes the σ-conservation step in the derivation that replaces the earlier skeleton with a real fixed-point result forced by the recognition cost. The result sits inside the broader φ-ladder construction but is specialized to the linguistic track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.