sqrt2_gt_14142
plain-language theorem explainer
The declaration proves 1.4142 < sqrt(2) in the reals. Researchers deriving upper bounds on the gap weight w8 or Fermi-constant predictions cite it to close decimal intervals. The tactic proof verifies non-negativity and the squared inequality via norm_num, then applies the right half of the Real.lt_sqrt lemma.
Claim. $1.4142 < 2^{1/2}$
background
The W8 Numerical Bounds module supplies tight decimal intervals for √2 and φ so that the closed-form gap weight w8 = (348 + 210√2 − (204 + 130√2)φ)/7 can be bounded rigorously; the expression evaluates to approximately 2.490569. These bounds are required to certify inequalities that appear in the Recognition Science constants derived from the eight-tick octave. The single upstream dependency is the for structure, which records the structural properties demanded by meta-realization of the self-reference axioms.
proof idea
The tactic proof first obtains (0 : ℝ) ≤ 1.4142 and 1.4142² < 2 by norm_num. It then applies the lemma Real.lt_sqrt in the direction that converts these two facts into the target strict inequality.
why it matters
The result is invoked inside w8_computed_lt to obtain the upper bound 2.490572090 on the gap weight and inside row_fermi_pred_upper to bound the predicted Fermi constant. It therefore supplies the numerical anchor that keeps the gap-weight verification aligned with the value obtained from the eight-tick octave (T7) in the Recognition framework. No open scaffolding questions are addressed by this bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.