sqrt5_gt_2_2
plain-language theorem explainer
The inequality 2.2 < sqrt(5) supplies a concrete lower bound on the golden ratio phi in Recognition Science numerical work. Researchers deriving phi-ladder mass formulas or tightening the alpha inverse interval cite it when converting the arithmetic definition of phi into explicit decimal bounds. The tactic proof squares both sides via norm_num, rewrites the target using the identity sqrt(x^2) = x for x nonnegative, and finishes with the monotonicity of the square root.
Claim. In the real numbers, $2.2 < 5^{1/2}$.
background
The module Support.PhiApprox supplies explicit numerical bounds on the golden ratio phi = (1 + sqrt(5))/2 that enter Recognition Science constants such as hbar = phi^{-5} and G = phi^5 / pi. The present lemma isolates a lower estimate on sqrt(5) that converts directly into phi > 1.6 through the arithmetic-mean expression. It works inside the standard real numbers imported from Mathlib and carries no extra hypotheses.
proof idea
norm_num first confirms that 2.2 squared is strictly less than 5. The proof then rewrites the right-hand side of the target inequality by the identity sqrt(2.2^2) = 2.2 (valid once nonnegativity is recorded) and applies Real.sqrt_lt_sqrt to the resulting comparison of squares.
why it matters
The lemma is invoked directly inside phi_gt_1_6 to obtain the bound 1.6 < phi. That bound in turn supports the phi-ladder rung calculations and the T6 self-similar fixed point of the UnifiedForcingChain. It closes a numerical gap needed for the eight-tick octave and the Berry creation threshold without importing external decimal expansions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.