phi_inv_lt_one
plain-language theorem explainer
The theorem shows that the reciprocal of the golden ratio is strictly less than one. Lexicon modelers using the Fibonacci recurrence for active and passive token counts cite this bound to keep the steady-state active fraction below unity. The proof is a direct term reduction that unfolds the reciprocal definition, rewrites via the division inequality under positivity, and invokes the lemma that the golden ratio exceeds one.
Claim. Let $phi$ be the golden ratio satisfying $phi^2 = phi + 1$. Then $phi^{-1} < 1$.
background
In the lexicon model a discrete-time recurrence on active tokens $a_n$ and passive tokens $p_n$ is given by $a_{n+1} = a_n + p_n$ and $p_{n+1} = a_n$, the Fibonacci recurrence. The active fraction $a_n / L_n$ converges to the fixed point $1/phi$ where $phi$ satisfies the quadratic identity. Upstream the identity $phi^{-1} = phi - 1$ is proved in the PhiRing and Inequalities modules, and the lemma one_lt_phi states $1 < phi$.
proof idea
Unfold the definition of phi_inv to obtain the division by phi. Rewrite the target inequality using the division-less-than-one rule under the positivity of phi supplied by Constants. Apply the lemma one_lt_phi to finish.
why it matters
The bound is invoked directly to prove lexicon_ratio_lt_one and passive_fraction_pos in the same module and to guarantee convergence of the geometric series in PhiEmergence. It anchors the fixed-point derivation of the active fraction in the sigma-conserving recurrence, consistent with the phi emergence forced by the T5 J-uniqueness step of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.