sqrt5_lt_2237
plain-language theorem explainer
This theorem proves that the square root of five is strictly less than 2.237. Researchers deriving numerical bounds on the golden ratio for Recognition Science applications would cite it to obtain an upper estimate on φ. The proof is a short term-mode reduction that rewrites the target via the square-root identity and applies monotonicity of the square root to the prior fact that 5 lies below 2.237 squared.
Claim. $√5 < 2.237$
background
The module supplies rigorous algebraic bounds on φ = (1 + √5)/2. Its strategy rests on the elementary comparison 2.236² < 5 < 2.237², which immediately yields 2.236 < √5 < 2.237 and therefore 1.618 < φ < 1.6185. The upstream lemma five_lt_sq_2237 asserts the right-hand inequality 5 < 2.237² and is obtained by direct numerical evaluation.
proof idea
The term proof first rewrites the goal using the identity √(x²) = x for x ≥ 0. It then applies sqrt_lt_sqrt to the pair of non-negative reals 0 and 5 together with the already-established comparison five_lt_sq_2237.
why it matters
The result is invoked directly by phi_lt_16185 to conclude φ < 1.6185. It therefore participates in the module’s chain of bounds that tighten the estimate of the golden ratio, the self-similar fixed point forced at step T6 of the Recognition Science forcing chain. The module documentation explicitly links these inequalities to the interval 1.618 < φ < 1.6185 used in later numerical work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.