phi_gt_onePointSixOne
plain-language theorem explainer
The golden ratio satisfies 1.61 < phi. Recognition Science applications that need a concrete numerical floor on phi, such as frequency bands on the phi-ladder or J-cost intervals, cite this bound. The proof is a short tactic sequence that unfolds the definition of phi, proves a square-root comparison by squaring, and closes with linarith.
Claim. $1.61 < phi$
background
In the Recognition framework phi is the self-similar fixed point forced at step T6 of the unified forcing chain, satisfying phi = 1 + 1/phi and appearing in the eight-tick octave and the phi-ladder mass formula. The Constants module supplies elementary real-arithmetic bounds on this number once its definition is fixed. Upstream results such as OptionAEmpiricalProgram.is and SimplicialLedger.EdgeLengthFromPsi.is supply the surrounding empirical and geometric setting in which the bound is later applied, though the present lemma itself uses only the definition of phi together with real-number comparison tactics.
proof idea
The proof unfolds the definition of phi via simp, then proves 2.22 < sqrt(5) by showing 2.22 squared is less than 5 with norm_num, rewriting the square-root inequality, and finishing with linarith.
why it matters
This lemma supplies the lower half of the tight numerical interval (1.61, 1.62) used by forty downstream declarations, including optimalT60_band (which places reverberation time inside the Beranek band), Jphi_numerical_band (which locates J(phi) inside (0.11, 0.12)), phi_eighth_in_gamma_band (which places phi^8 inside the gamma EEG range), and E_PBM_bounds. It therefore supports the concrete numerical predictions that follow from the eight-tick octave and the phi-ladder once phi is fixed as the T6 fixed point. No open scaffolding questions are discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.