five_lt_sq_22360680
plain-language theorem explainer
Establishing 5 < 2.2360680 squared supplies the numerical anchor for bounding √5 from below inside the golden ratio interval module. Researchers tightening decimal approximations to φ would cite it when constructing rigorous lower bounds on the square root. The proof is a direct term-mode invocation of the norm_num tactic that confirms the floating-point comparison by computation.
Claim. In the real numbers, $5 < 2.2360680^2$.
background
The module Numerics.Interval.PhiBounds supplies rigorous bounds on the golden ratio φ = (1 + √5)/2. Its strategy rests on verifying concrete decimal comparisons such as 2.236² = 4.999696 < 5 < 5.001956 = 2.237², which yields 2.236 < √5 < 2.237 and therefore 1.618 < φ < 1.6185. Tighter bounds are obtained by extending the decimal expansions.
proof idea
The proof is a one-line term that applies the norm_num tactic to discharge the inequality by direct numerical evaluation.
why it matters
This theorem is invoked by sqrt5_lt_22360680 to conclude √5 < 2.2360680, completing one side of the interval for √5. It thereby supports the module's construction of bounds on φ, which aligns with the Recognition Science derivation of phi as the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.