sqrt5_gt_2236
plain-language theorem explainer
2.236 < √5 anchors the lower estimate for deriving φ > 1.618 from the definition φ = (1 + √5)/2. Numerics code in the Recognition framework cites this when establishing decimal bounds on the golden ratio without floating-point reliance. The term proof rewrites via the square-root identity and applies sqrt_lt_sqrt directly to the upstream square inequality.
Claim. $2.236 < √5$
background
The module supplies rigorous algebraic bounds on φ = (1 + √5)/2. Its strategy compares squares to obtain 2.236 < √5 < 2.237, which immediately yields 1.618 < φ < 1.6185. The upstream lemma sq_2236_lt_5 asserts (2.236 : ℝ)^2 < 5 and is discharged by norm_num.
proof idea
The term proof rewrites the target as √(2.236²) < √5 using the identity √(x²) = x for nonnegative x, then invokes sqrt_lt_sqrt on the norm_num fact (2.236 : ℝ)^2 < 5 supplied by sq_2236_lt_5.
why it matters
This result is invoked by phi_gt_1618 to obtain 1.618 < φ. It supplies the first concrete decimal step in the module's bounding strategy for the self-similar fixed point φ that appears in the forcing chain and phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.