sq_2236_lt_5
plain-language theorem explainer
The inequality (2.236)^2 < 5 supplies a concrete lower bound on sqrt(5) in the reals. Numerics work on golden-ratio intervals for Recognition Science constants cites this to start the chain 2.236 < sqrt(5) < 2.237. The proof is a direct term-mode call to norm_num that evaluates the floating-point comparison.
Claim. $ (2.236)^2 < 5 $
background
The module supplies rigorous bounds on φ = (1 + √5)/2 by verifying algebraic inequalities on decimal approximations. The explicit strategy is to establish 2.236² < 5 < 2.237², deduce 2.236 < √5 < 2.237, and obtain 1.618 < φ < 1.6185, with tighter bounds obtained by adding decimal places. No upstream lemmas are invoked; the result rests only on the ordered field axioms of the reals.
proof idea
The proof is a one-line term-mode wrapper that invokes the norm_num tactic to confirm the numerical inequality by direct evaluation.
why it matters
This theorem is the first link in the interval chain that produces sqrt5_gt_2236 and the subsequent bounds on φ. It anchors the numerical constants appearing in the phi-ladder mass formula and the alpha inverse interval (137.030, 137.039) used throughout the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.