sqrt5_lt_22360680
plain-language theorem explainer
The inequality √5 < 2.2360680 holds over the reals. Researchers establishing decimal bounds on the golden ratio φ = (1 + √5)/2 cite this result to control approximation error in the phi-ladder numerics. The term proof rewrites the target via the identity √(x²) = x for x ≥ 0, then applies monotonicity of sqrt to the companion fact 5 < (2.2360680)².
Claim. In the real numbers, the square root of five satisfies $√5 < 2.2360680$.
background
The module supplies rigorous decimal bounds on φ = (1 + √5)/2 by sandwiching √5 between nearby rationals whose squares bracket 5. The upstream theorem five_lt_sq_22360680 states that 5 < (2.2360680)² and is obtained by direct norm_num evaluation. These bounds feed the strategy 2.2360680² < 5 < 2.2360681² to produce 1.618 < φ < 1.6185 and tighter variants.
proof idea
The term proof first rewrites the goal using the identity √(x²) = x for nonnegative x. It then invokes the lemma that sqrt is strictly increasing on the nonnegative reals, reducing the claim to the already-proved inequality 5 < (2.2360680)².
why it matters
The result supplies the numerical anchor for the sibling theorem phi_lt_16180340 that asserts φ < 1.6180340. It supports the Recognition Science treatment of φ as the self-similar fixed point forced in the T0–T8 chain and the phi-ladder mass formula. No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.