phi_inv_pos
plain-language theorem explainer
The active fraction of a lexicon evolving under Fibonacci recurrence is strictly positive. Linguists modeling vocabulary growth or physicists deriving constants from recognition cost would cite this result. The proof is a one-line wrapper applying the positivity of division to the unit and the positivity of the golden ratio.
Claim. Let $r$ denote the predicted active-vocabulary fraction. Then $0 < r$, where $r = 1/φ$ and $φ$ is the golden ratio.
background
The module derives the active/passive lexicon ratio from a Fibonacci-style recurrence on a two-state model. Active tokens at step $n+1$ equal the sum of active and passive at $n$, while passive at $n+1$ equals active at $n$. The ratio of active tokens to total lexicon size converges to the fixed point $1/φ$ from the identity $φ^2 = φ + 1$.
proof idea
The proof is a one-line wrapper applying the positivity of division lemma to the fact that 1 is positive and the golden ratio is positive.
why it matters
This positivity result is invoked by the lexicon ratio positivity theorem and the uniqueness theorem for the fixed point $x + x^2 = 1$. It supports the claim that the active fraction is $1/φ$ in the linguistic model derived from recognition cost. In the broader framework it aligns with the phi emergence and provides a basic inequality needed for series convergence arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.