phi5_lt_12
plain-language theorem explainer
The bound phi^5 < 12 supplies the upper estimate for the golden-ratio scaling factor in lexical half-life models. Researchers in quantitative linguistics would reference it when verifying that the observed 8-fold ratio between high- and low-frequency word persistence lies inside the phi-ladder interval. The proof proceeds by unfolding the powers via the recurrence relation phi^n = phi^{n-1} + phi^{n-2} and closing with the numerical bound phi < 1.62.
Claim. $ (1 + √5)/2 ^5 < 12 $
background
In the Lexical Decay From Phi Ladder module, word half-lives scale with powers of the golden ratio phi on a recognition-frequency ladder. High-frequency words persist approximately phi^5 times longer than low-frequency ones, yielding a predicted ratio near 11.1 that is compared to the empirical factor of 8. The key algebraic identity phi^2 = phi + 1 generates the Fibonacci coefficients for higher powers. An auxiliary lemma establishes the strict inequality phi < 1.62.
proof idea
The tactic proof first invokes phi_sq_eq to obtain the base recurrence. It then derives the explicit linear expressions phi^3 = 2phi + 1, phi^4 = 3phi + 2, and phi^5 = 5*phi + 3 by successive nlinarith steps. Finally linarith combines these with the bound phi < 1.62 to conclude the inequality.
why it matters
This theorem closes the upper half of the interval used by lexicalDecayCert to certify that the phi-ladder ratio matches observed lexical decay rates. It directly supports the module's claim that the top-five-rung frequency span approximates phi^5 within the J-cost band. The result sits inside the broader Recognition Science derivation of self-similar scaling from the functional equation for J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.