Numerics Interval W8 Bounds Sqrt2 Gt 14142

A decimal bound for √2

The square root of 2, the number that when multiplied by itself gives 2, is irrational: its decimal expansion never repeats and never ends. Its value is about 1.41421356, but for many calculations a precise decimal window is more useful than the full expansion. A theorem in the framework's machine-checked library of formal theorems establishes one such window: the real number 1.4142 is less than √2, and a companion theorem shows √2 is less than 1.4143. Together they prove that √2 lies strictly between those two four-decimal bounds.

The proof is not a numerical approximation from a calculator. It is a formal argument that starts from the definition of the real square root and verifies the claim by checking that 1.4142 squared is less than 2, while 1.4143 squared is greater than 2. Because the real numbers are ordered, those two inequalities force the square root to sit between the bounds. The library records this as a theorem, meaning the reasoning has been checked step by step by a machine, with no gaps and no hidden assumptions beyond the standard axioms of the underlying logic.

This bound is part of a larger project inside the framework. The framework's account of recognition, a discrete record of events, produces a quantity called the gap weight w8, a numerical value tied to an eight-tick cycle. The library computes w8 from a closed formula involving √2 and the golden ratio, and the bounds on √2 help pin down w8 to a tight interval. The theorems here are the numerical scaffolding: they guarantee that later statements about w8 rest on exact inequalities, not on rounded arithmetic.

What the declaration does not claim is just as important. It does not say that √2 is rational, nor does it provide any new mathematical property of the number. It only certifies a specific decimal window. It also does not, by itself, say anything about the gap weight w8; the connection comes only through the larger file that uses these bounds. The theorem is a small, verified fact, valuable for the precision it guarantees and for nothing more.

/-- Lower decimal bound for √2. -/
theorem sqrt2_gt_14142 : (1.4142 : ℝ) < Real.sqrt 2 := by
  have hx : (0 : ℝ) ≤ (1.4142 : ℝ) := by norm_num
  have hsq : (1.4142 : ℝ) ^ 2 < (2 : ℝ) := by norm_num
  exact (Real.lt_sqrt hx).2 hsq

/-- Upper decimal bound for √2. -/
theorem sqrt2_lt_14143 : Real.sqrt 2 < (1.4143 : ℝ) := by
  have hx : (0 : ℝ) ≤ (2 : ℝ) := by norm_num
  have hy : (0 : ℝ) ≤ (1.4143 : ℝ) := by norm_num
  have hsq : (2 : ℝ) < (1.4143 : ℝ) ^ 2 := by norm_num
  exact (Real.sqrt_lt hx hy).2 hsq

What this page does not claim

The theorem does not claim any new property of √2 beyond its decimal bounds. It does not claim that √2 is rational or irrational. It does not, by itself, establish anything about the gap weight w8.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Numerics/Interval/W8Bounds.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: