five_lt_sq_2237
plain-language theorem explainer
The theorem establishes the strict inequality 5 < 2.237 squared over the reals. Numerics work on decimal bounds for the golden ratio cites it to anchor the upper estimate on sqrt(5) before passing to phi. The proof is a direct norm_num computation that verifies the decimal arithmetic without further lemmas.
Claim. $5 < (2.237)^2$
background
This declaration belongs to the Numerics.Interval.PhiBounds module, whose purpose is to supply rigorous bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties of the reals. The module strategy starts from the concrete decimal inequalities 2.236² < 5 < 2.237², which immediately yield 2.236 < √5 < 2.237 and therefore 1.618 < φ < 1.6185; tighter bounds are obtained by carrying more decimal places. No upstream results are required; the declaration stands alone as a verified numerical fact.
proof idea
The proof is a one-line wrapper that invokes the norm_num tactic to check the floating-point inequality directly.
why it matters
It is the immediate premise for the downstream theorem sqrt5_lt_2237, which rewrites the target sqrt(5) < 2.237 via sqrt_sq and sqrt_lt_sqrt. In the Recognition Science setting the result supplies the numerical anchor for φ as the self-similar fixed point (T6) on the phi-ladder that enters mass formulas, the constant ħ = φ^{-5}, and the eight-tick octave structure. It closes a small but necessary scaffolding step for decimal precision inside the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.