sqrt5_lt_2_4
plain-language theorem explainer
The lemma establishes that sqrt(5) is strictly less than 2.4 over the reals. It is invoked by the sibling bound phi_lt_1_7 to cap the golden ratio below 1.7. The proof reduces the target inequality to a comparison of squares and applies the monotonicity of the square root on the non-negative reals.
Claim. $√5 < 2.4$
background
The Support.PhiApprox module supplies concrete numerical bounds on the golden ratio for later Recognition Science calculations. Constants.phi is defined as the positive root of x² - x - 1 = 0, equivalently (1 + √5)/2. This lemma supplies a sufficient upper bound on √5 that feeds directly into the proof of phi < 1.7. No upstream lemmas are required; the argument uses only standard real-analysis facts imported from Mathlib.
proof idea
The tactic proof first invokes norm_num to obtain 5 < 2.4². It records non-negativity of both 5 and 2.4. The right-hand side is rewritten via the identity √(a²) = a for a ≥ 0. The goal then reduces to showing √5 < 2.4, which follows at once from the strict increase of the square-root function on the non-negative reals.
why it matters
The result is used by phi_lt_1_7 to conclude Constants.phi < 1.7 by rewriting 1.7 as (1 + 2.4)/2 and applying linarith. Within the Recognition Science framework it anchors the self-similar fixed point phi (T6) with a verifiable numerical bound that supports the phi-ladder mass formula and the eight-tick octave. It closes a minor numerical gap in the support layer without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.