sqrt2_lt_14143
plain-language theorem explainer
Upper decimal bound sqrt(2) < 1.4143 supports interval arithmetic for the gap weight w8 in the eight-tick octave. Workers on the Fermi constant scorecard and w8 bounds invoke it to certify the phi-ladder numerics. The proof reduces the claim to a squared comparison using the sqrt monotonicity lemma after norm_num checks.
Claim. $sqrt(2) < 1.4143$ holds in the reals.
background
The W8Bounds module supplies decimal intervals for sqrt(2) and phi to certify the closed-form gap weight w8_from_eight_tick = (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7. This expression encodes the eight-tick octave period from the forcing chain T7. The local setting uses these bounds to keep all numerical claims about w8 provable inside the Recognition Science constants.
proof idea
The tactic proof first uses norm_num to obtain non-negativity of 2 and of 1.4143. It then uses norm_num again to confirm 2 < (1.4143)^2. The final step applies the right-to-left direction of Real.sqrt_lt to the squared inequality.
why it matters
The bound is used in w8_computed_gt to obtain the strict lower estimate 2.490564399 < w8_from_eight_tick and in row_fermi_pred_lower for the Fermi constant prediction. It closes a numerical link in the eight-tick octave (T7) and the phi-ladder mass formula. No open scaffolding remains for this decimal interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.