Encyclopedia Numerics Numerics Interval W8 Bounds Sqrt2 Lt 14143

ARTICLE 4 claims 3 theorems 1 model

Numerics Interval W8 Bounds Sqrt2 Lt 14143

The square root of 2 is less than 1.4143, and a machine-checked proof pins that down exactly.

Verify this page

A narrow bound

The square root of 2, the number that multiplied by itself gives 2, is about 1.41421356. The declaration sqrt2_lt_14143 proves the upper half of a two-sided bound: it is less than 1.4143. Its companion sqrt2_gt_14142 proves the lower half, so together they trap the value between 1.4142 and 1.4143. That interval is wide enough to be unremarkable, but the proof method is the point: each inequality is checked by squaring the decimal and comparing the square to 2, with no appeal to decimal expansion tables or calculators.

In the Recognition Science framework, these bounds serve a concrete purpose. The framework's eight-tick cycle assigns a weight to the eighth gap, written w8_from_eight_tick (a number attached to the eighth step of the recognition cycle). That weight is defined by a closed formula involving both √2 and the golden ratio φ: w8 = (348 + 210√2 − (204 + 130√2)φ)/7. To use this weight in further calculations, the framework needs rigorous numerical bounds for both constants. The two √2 inequalities, together with similar bounds for φ (between 1.61803395 and 1.6180340), feed into interval arithmetic that brackets the weight between 2.490564399 and 2.490572090.

What the declaration does not claim is just as precise. It does not say √2 is irrational, transcendental, or anything about its decimal expansion beyond the stated inequality. It does not assert that the bound is sharp or optimal; 1.4143 is merely a convenient decimal upper limit. It also does not by itself say anything about the physical meaning of the weight w8; that meaning comes from other parts of the framework. The theorem is a narrow, fully verified numerical fact, useful because it is exact.

For a reader, the practical takeaway is that the framework's numerical constants are not hand-waved. Every decimal bound used in the weight calculation is backed by a machine-checked proof, so the interval for w8 is not an approximation but a proven containment. That is what makes the later use of the interval trustworthy: the bracket is not a guess, it is a theorem.

THEOREM sqrt2_lt_14143 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
sqrt2_lt_14143 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:31 
/-- 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
THEOREM sqrt2_gt_14142 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
sqrt2_gt_14142 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:25 
/-- 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
THEOREM w8_computed_gt · w8_computed_lt · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
w8_computed_gt · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:57 
/-- The gap weight is greater than 2.490564399. -/
theorem w8_computed_gt : (2.490564399 : ℝ) < IndisputableMonolith.Constants.w8_from_eight_tick := by
  -- w8 = (348 + 210√2 - (204 + 130√2)φ)/7
  have hs2_hi : Real.sqrt 2 ≤ (1.4143 : ℝ) := le_of_lt sqrt2_lt_14143
  have hφ_hi : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := phi_lt_16180340

  -- Step 1: replace φ by its upper bound (expression decreases as φ increases).
  have h_phi_step :
      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) / 7
        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7 := by
    have hA : 0 ≤ (204 : ℝ) + 130 * Real.sqrt 2 := by
      have : (0 : ℝ) ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
      nlinarith
    have hmul :
        -((204 : ℝ) + 130 * Real.sqrt 2) * (1.6180340 : ℝ)
          ≤ -((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi := by
      have hnegA : -((204 : ℝ) + 130 * Real.sqrt 2) ≤ 0 := by linarith
      -- phi ≤ 1.6180340 and the coefficient is nonpositive, so inequality flips.
      exact mul_le_mul_of_nonpos_left hφ_hi.le hnegA
    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
    have hnum :
        (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * (1.6180340 : ℝ)
          ≤ (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi := by
      linarith [hmul]
    exact (div_le_div_of_nonneg_right hnum (le_of_lt h7))

  -- Step 2: with φ fixed at its max, the expression decreases in √2 because (210 - 130φ) < 0.
  have hcoeff_neg : (210 : ℝ) - 130 * (1.6180340 : ℝ) < 0 := by norm_num
  have h_s2_step :
      (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7
        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) / 7 := by
    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
    -- Rewrite numerator as `A + √2 * B` where `B < 0`, so replacing √2 by its upper bound
    -- gives a *lower* value (hence a lower corner bound).
    set B : ℝ := (210 : ℝ) - 130 * (1.6180340 : ℝ)
    have hB : B ≤ 0 := by
      have : B < 0 := by simpa [B] using hcoeff_neg
      exact le_of_lt this
    have hs2_term : (1.4143 : ℝ) * B ≤ Real.sqrt 2 * B := by
      have hs : Real.sqrt 2 ≤ (1.4143 : ℝ) := hs2_hi
      exact mul_le_mul_of_nonpos_right hs hB
    have hnum_raw :
        (348 : ℝ) - 204 * (1.6180340 : ℝ) + (1.4143 : ℝ) * B
          ≤ (348 : ℝ) - 204 * (1.6180340 : ℝ) + Real.sqrt 2 * B := by
      linarith [hs2_term]
    have hrewL :
        (348 : ℝ) - 204 * (1.6180340 : ℝ) + (1.4143 : ℝ) * B
          = (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) := by
      simp [B]
      ring
    have hrewR :
        (348 : ℝ) - 204 * (1.6180340 : ℝ) + Real.sqrt 2 * B
          = (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) := by
      simp [B]
      ring
    have hnum' :
        (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ))
          ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) := by
      simpa [hrewL, hrewR] using hnum_raw
    exact (div_le_div_of_nonneg_right hnum' (le_of_lt h7))

  -- Combine the steps.
  have hw8_corner :
      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7
        ≥ (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7 :=
    -- corner ≤ (φ_hi,sqrt2) ≤ (φ,sqrt2)
    show (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7
          ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7 from
      le_trans h_s2_step h_phi_step

  -- Now the numeric corner value is > 2.490564399.
  have hcorner_gt :
      (2.490564399 : ℝ) <
        (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7 := by
    norm_num

  -- Finish by unfolding w8 and chaining inequalities.
  unfold IndisputableMonolith.Constants.w8_from_eight_tick
  exact lt_of_lt_of_le hcorner_gt hw8_corner
w8_computed_lt · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:137 
/-- The gap weight is less than 2.490572090. -/
theorem w8_computed_lt : IndisputableMonolith.Constants.w8_from_eight_tick < (2.490572090 : ℝ) := by
  -- Upper bound by the “best-case corner” (√2 minimal, φ minimal).
  have hs2_lo : (1.4142 : ℝ) ≤ Real.sqrt 2 := le_of_lt sqrt2_gt_14142
  have hφ_lo : (1.61803395 : ℝ) ≤ IndisputableMonolith.Constants.phi := by
    exact le_of_lt phi_gt_161803395

  -- Step 1: replace φ by its lower bound (expression increases as φ decreases).
  have h_phi_step :
      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7
        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ)) / 7 := by
    have hA : 0 ≤ (204 : ℝ) + 130 * Real.sqrt 2 := by
      have : (0 : ℝ) ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
      nlinarith
    have hmul :
        -((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi
          ≤ -((204 : ℝ) + 130 * Real.sqrt 2) * (1.61803395 : ℝ) := by
      have hnegA : -((204 : ℝ) + 130 * Real.sqrt 2) ≤ 0 := by linarith
      exact mul_le_mul_of_nonpos_left hφ_lo hnegA
    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
    have hnum :
        (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi
          ≤ (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * (1.61803395 : ℝ) := by
      linarith [hmul]
    exact (div_le_div_of_nonneg_right hnum (le_of_lt h7))

  -- Step 2: with φ fixed at its min, the expression increases in √2 because (210 - 130φ) < 0,
  -- so taking √2 at its lower bound gives an upper bound for the whole expression.
  have hcoeff_neg : (210 : ℝ) - 130 * (1.61803395 : ℝ) < 0 := by norm_num
  have h_s2_step :
      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ)) / 7
        ≤ (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) / 7 := by
    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
    have hs2_term :
        Real.sqrt 2 * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
          ≤ (1.4142 : ℝ) * ((210 : ℝ) - 130 * (1.61803395 : ℝ)) := by
      have : (1.4142 : ℝ) ≤ Real.sqrt 2 := hs2_lo
      have hcoeff_nonpos : ((210 : ℝ) - 130 * (1.61803395 : ℝ)) ≤ 0 := le_of_lt hcoeff_neg
      exact mul_le_mul_of_nonpos_right this hcoeff_nonpos
    have hnum :
        (348 : ℝ) - 204 * (1.61803395 : ℝ) + Real.sqrt 2 * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
          ≤ (348 : ℝ) - 204 * (1.61803395 : ℝ) + (1.4142 : ℝ) * ((210 : ℝ) - 130 * (1.61803395 : ℝ)) := by
      linarith
    have hrew1 :
        (348 : ℝ) - 204 * (1.61803395 : ℝ) + Real.sqrt 2 * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
          = (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ)) := by
      ring
    have hrew2 :
        (348 : ℝ) - 204 * (1.61803395 : ℝ) + (1.4142 : ℝ) * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
          = (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) := by
      ring
    have hnum' :
        (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ))
          ≤ (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) := by
      simpa [hrew1, hrew2] using hnum
    exact (div_le_div_of_nonneg_right hnum' (le_of_lt h7))

  -- Combine the steps.
  have hw8_corner :
      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7
        ≤ (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) / 7 :=
    le_trans h_phi_step h_s2_step

  -- Now the numeric corner value is < 2.490572090.
  have hcorner_lt :
      (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) / 7 < (2.490572090 : ℝ) := by
    norm_num

  -- Finish by unfolding w8 and chaining inequalities.
  unfold IndisputableMonolith.Constants.w8_from_eight_tick
  exact lt_of_le_of_lt hw8_corner hcorner_lt

What this page does not claim

This does not claim that 1.4143 is a sharp or optimal upper bound for √2. This does not claim that the w8 weight has any physical interpretation beyond its definition in the framework. This does not claim that the decimal bounds for √2 or φ are derived from the forcing chain; they are proven directly from the real number axioms.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND