phi_inv_band
plain-language theorem explainer
The theorem proves that the inverse golden ratio satisfies 0.6 < phi_inv < 0.7. Linguists modeling lexicon evolution via Fibonacci recurrences cite the bound to constrain the steady-state active token fraction. The proof unfolds the definition of phi_inv and applies the known bounds 1.5 < phi < 1.62 together with division rules and linear arithmetic.
Claim. $0.6 < phi^{-1} < 0.7$
background
In the LexiconRatio module a lexicon evolves over discrete time with active tokens a_n and passive tokens p_n obeying the sigma-conserving recurrence a_{n+1} = a_n + p_n, p_{n+1} = a_n. This is the Fibonacci recurrence whose total size grows as L_n ~ phi^n; the active fraction converges to the unique fixed point r = 1/phi satisfying r + r^2 = 1. The upstream theorem phi_inv from Algebra.PhiRing states phi^{-1} = phi - 1, while Constants supplies the tighter bounds phi > 1.5 and phi < 1.62 together with phi_pos.
proof idea
The term proof unfolds phi_inv, invokes Constants.phi_gt_onePointFive, Constants.phi_lt_onePointSixTwo and Constants.phi_pos, then applies lt_div_iff_0 to each side and closes both goals with linarith.
why it matters
lexicon_ratio_band applies this result verbatim to obtain the identical interval for the lexicon ratio. The bound supplies the numerical verification of the Fibonacci fixed-point identity that derives the active fraction from sigma-conservation in the 2-state lexicon model. It thereby closes the numerical step linking the recurrence to the self-similar fixed point of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.