sqrt5_gt_22360679
plain-language theorem explainer
Establishes the strict inequality 2.2360679 < √5 over the reals. Numerics work on golden-ratio bounds cites it to anchor lower estimates for φ without floating-point error. The term proof reduces the claim to an upstream square comparison by rewriting the left side as sqrt of its square and invoking monotonicity of sqrt on the positives.
Claim. $2.2360679 < √5$
background
The module supplies rigorous decimal bounds on the golden ratio φ = (1 + √5)/2. It proceeds by squaring candidate decimals to compare against 5, then taking square roots to bound √5 before averaging to bound φ. The upstream result sq_22360679_lt_5 states that (2.2360679 : ℝ)^2 < 5 and is discharged by norm_num.
proof idea
The term proof first rewrites the target via sqrt_sq using nonnegativity of 2.2360679. It then applies sqrt_lt_sqrt to the upstream square inequality sq_22360679_lt_5, which norm_num already verifies.
why it matters
This bound is invoked directly by the parent theorem phi_gt_161803395 to obtain 1.61803395 < φ. It supplies a concrete numerical anchor for the phi-ladder and the self-similar fixed point in the T0–T8 forcing chain. The module strategy of successive decimal tightenings supports the Recognition Science constants including the alpha inverse interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.