one_lt_phiPointSixOne
plain-language theorem explainer
The lemma establishes that the golden ratio exceeds 1.6. Researchers modeling phi-ladder quantities in urban settlement ratios, thermohaline timescales, and injury-risk thresholds cite the bound to anchor derived expressions inside measured intervals. The proof reduces directly from the stricter inequality phi greater than 1.61 via linear arithmetic.
Claim. $1.6 < phi$ where $phi = (1 + sqrt(5))/2$ denotes the golden ratio.
background
Recognition Science obtains the golden ratio as the unique positive fixed point of the J-cost map satisfying the Recognition Composition Law. The Constants module records a sequence of decimal bounds on phi that support rung-spacing calculations on the phi-ladder. Upstream, one_lt_phi supplies the basic fact 1 less than phi while phi_gt_onePointSixOne tightens the lower bound to 1.61; both rest on the algebraic definition of phi and elementary properties of the square root.
proof idea
The proof is a one-line wrapper that applies linarith to the hypothesis phi_gt_onePointSixOne.
why it matters
The bound is invoked inside settlementPopRatio_in_Christaller_band to verify that settlement population ratios lie between 3 and 8, inside amocTimescale_in_band to locate the overturning circulation timescale between 20 and 100 years, and inside injuryTipPoint_in_band to place the injury tip point between 1.4 and 1.9. It therefore supplies the concrete numerical anchor that connects the abstract T6 fixed-point construction to the empirical bands required by the T7-T8 octave and spatial-dimension steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.