IndisputableMonolith.Numerics.Interval.W8Bounds

   1-- import IndisputableMonolith.Numerics.Interval.Basic  -- [not in public release]
   2-- import IndisputableMonolith.Numerics.Interval.PiBounds  -- [not in public release]
   3-- import IndisputableMonolith.Numerics.Interval.PhiBounds  -- [not in public release]
   4import IndisputableMonolith.Constants.GapWeight
   5
   6namespace IndisputableMonolith.Numerics
   7namespace W8Bounds
   8
   9open Interval
  10open IndisputableMonolith.Constants
  11
  12/-!
  13## W8 Numerical Bounds
  14
  15The gap weight `w8_from_eight_tick` is approximately 2.490569.
  16
  17In the Lean codebase, `w8_from_eight_tick` is defined as a parameter‑free
  18closed form:
  19
  20`w8 = (348 + 210√2 - (204 + 130√2)φ)/7`.
  21
  22These theorems provide rigorous bounds using tight intervals for `φ` and `√2`.
  23-/
  24
  25/-- Lower decimal bound for √2. -/
  26theorem sqrt2_gt_14142 : (1.4142 : ℝ) < Real.sqrt 2 := by
  27  have hx : (0 : ℝ) ≤ (1.4142 : ℝ) := by norm_num
  28  have hsq : (1.4142 : ℝ) ^ 2 < (2 : ℝ) := by norm_num
  29  exact (Real.lt_sqrt hx).2 hsq
  30
  31/-- Upper decimal bound for √2. -/
  32theorem sqrt2_lt_14143 : Real.sqrt 2 < (1.4143 : ℝ) := by
  33  have hx : (0 : ℝ) ≤ (2 : ℝ) := by norm_num
  34  have hy : (0 : ℝ) ≤ (1.4143 : ℝ) := by norm_num
  35  have hsq : (2 : ℝ) < (1.4143 : ℝ) ^ 2 := by norm_num
  36  exact (Real.sqrt_lt hx hy).2 hsq
  37
  38/-- Lower decimal bound for φ. -/
  39theorem phi_gt_161803395 : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := by
  40  have hx : (0 : ℝ) ≤ (2.2360679 : ℝ) := by norm_num
  41  have hsq : (2.2360679 : ℝ) ^ 2 < (5 : ℝ) := by norm_num
  42  have hsqrt : (2.2360679 : ℝ) < Real.sqrt 5 := by
  43    exact (Real.lt_sqrt hx).2 hsq
  44  unfold IndisputableMonolith.Constants.phi
  45  linarith
  46
  47/-- Upper decimal bound for φ. -/
  48theorem phi_lt_16180340 : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := by
  49  have hx : (0 : ℝ) ≤ (5 : ℝ) := by norm_num
  50  have hy : (0 : ℝ) ≤ (2.236068 : ℝ) := by norm_num
  51  have hsq : (5 : ℝ) < (2.236068 : ℝ) ^ 2 := by norm_num
  52  have hsqrt : Real.sqrt 5 < (2.236068 : ℝ) := by
  53    exact (Real.sqrt_lt hx hy).2 hsq
  54  unfold IndisputableMonolith.Constants.phi
  55  linarith
  56
  57/-- The gap weight is greater than 2.490564399. -/
  58theorem w8_computed_gt : (2.490564399 : ℝ) < IndisputableMonolith.Constants.w8_from_eight_tick := by
  59  -- w8 = (348 + 210√2 - (204 + 130√2)φ)/7
  60  have hs2_hi : Real.sqrt 2 ≤ (1.4143 : ℝ) := le_of_lt sqrt2_lt_14143
  61  have hφ_hi : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := phi_lt_16180340
  62
  63  -- Step 1: replace φ by its upper bound (expression decreases as φ increases).
  64  have h_phi_step :
  65      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) / 7
  66        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7 := by
  67    have hA : 0 ≤ (204 : ℝ) + 130 * Real.sqrt 2 := by
  68      have : (0 : ℝ) ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
  69      nlinarith
  70    have hmul :
  71        -((204 : ℝ) + 130 * Real.sqrt 2) * (1.6180340 : ℝ)
  72          ≤ -((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi := by
  73      have hnegA : -((204 : ℝ) + 130 * Real.sqrt 2) ≤ 0 := by linarith
  74      -- phi ≤ 1.6180340 and the coefficient is nonpositive, so inequality flips.
  75      exact mul_le_mul_of_nonpos_left hφ_hi.le hnegA
  76    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
  77    have hnum :
  78        (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * (1.6180340 : ℝ)
  79          ≤ (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi := by
  80      linarith [hmul]
  81    exact (div_le_div_of_nonneg_right hnum (le_of_lt h7))
  82
  83  -- Step 2: with φ fixed at its max, the expression decreases in √2 because (210 - 130φ) < 0.
  84  have hcoeff_neg : (210 : ℝ) - 130 * (1.6180340 : ℝ) < 0 := by norm_num
  85  have h_s2_step :
  86      (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7
  87        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) / 7 := by
  88    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
  89    -- Rewrite numerator as `A + √2 * B` where `B < 0`, so replacing √2 by its upper bound
  90    -- gives a *lower* value (hence a lower corner bound).
  91    set B : ℝ := (210 : ℝ) - 130 * (1.6180340 : ℝ)
  92    have hB : B ≤ 0 := by
  93      have : B < 0 := by simpa [B] using hcoeff_neg
  94      exact le_of_lt this
  95    have hs2_term : (1.4143 : ℝ) * B ≤ Real.sqrt 2 * B := by
  96      have hs : Real.sqrt 2 ≤ (1.4143 : ℝ) := hs2_hi
  97      exact mul_le_mul_of_nonpos_right hs hB
  98    have hnum_raw :
  99        (348 : ℝ) - 204 * (1.6180340 : ℝ) + (1.4143 : ℝ) * B
 100          ≤ (348 : ℝ) - 204 * (1.6180340 : ℝ) + Real.sqrt 2 * B := by
 101      linarith [hs2_term]
 102    have hrewL :
 103        (348 : ℝ) - 204 * (1.6180340 : ℝ) + (1.4143 : ℝ) * B
 104          = (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) := by
 105      simp [B]
 106      ring
 107    have hrewR :
 108        (348 : ℝ) - 204 * (1.6180340 : ℝ) + Real.sqrt 2 * B
 109          = (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) := by
 110      simp [B]
 111      ring
 112    have hnum' :
 113        (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ))
 114          ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) := by
 115      simpa [hrewL, hrewR] using hnum_raw
 116    exact (div_le_div_of_nonneg_right hnum' (le_of_lt h7))
 117
 118  -- Combine the steps.
 119  have hw8_corner :
 120      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7
 121        ≥ (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7 :=
 122    -- corner ≤ (φ_hi,sqrt2) ≤ (φ,sqrt2)
 123    show (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7
 124          ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7 from
 125      le_trans h_s2_step h_phi_step
 126
 127  -- Now the numeric corner value is > 2.490564399.
 128  have hcorner_gt :
 129      (2.490564399 : ℝ) <
 130        (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7 := by
 131    norm_num
 132
 133  -- Finish by unfolding w8 and chaining inequalities.
 134  unfold IndisputableMonolith.Constants.w8_from_eight_tick
 135  exact lt_of_lt_of_le hcorner_gt hw8_corner
 136
 137/-- The gap weight is less than 2.490572090. -/
 138theorem w8_computed_lt : IndisputableMonolith.Constants.w8_from_eight_tick < (2.490572090 : ℝ) := by
 139  -- Upper bound by the “best-case corner” (√2 minimal, φ minimal).
 140  have hs2_lo : (1.4142 : ℝ) ≤ Real.sqrt 2 := le_of_lt sqrt2_gt_14142
 141  have hφ_lo : (1.61803395 : ℝ) ≤ IndisputableMonolith.Constants.phi := by
 142    exact le_of_lt phi_gt_161803395
 143
 144  -- Step 1: replace φ by its lower bound (expression increases as φ decreases).
 145  have h_phi_step :
 146      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7
 147        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ)) / 7 := by
 148    have hA : 0 ≤ (204 : ℝ) + 130 * Real.sqrt 2 := by
 149      have : (0 : ℝ) ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
 150      nlinarith
 151    have hmul :
 152        -((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi
 153          ≤ -((204 : ℝ) + 130 * Real.sqrt 2) * (1.61803395 : ℝ) := by
 154      have hnegA : -((204 : ℝ) + 130 * Real.sqrt 2) ≤ 0 := by linarith
 155      exact mul_le_mul_of_nonpos_left hφ_lo hnegA
 156    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
 157    have hnum :
 158        (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi
 159          ≤ (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * (1.61803395 : ℝ) := by
 160      linarith [hmul]
 161    exact (div_le_div_of_nonneg_right hnum (le_of_lt h7))
 162
 163  -- Step 2: with φ fixed at its min, the expression increases in √2 because (210 - 130φ) < 0,
 164  -- so taking √2 at its lower bound gives an upper bound for the whole expression.
 165  have hcoeff_neg : (210 : ℝ) - 130 * (1.61803395 : ℝ) < 0 := by norm_num
 166  have h_s2_step :
 167      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ)) / 7
 168        ≤ (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) / 7 := by
 169    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
 170    have hs2_term :
 171        Real.sqrt 2 * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
 172          ≤ (1.4142 : ℝ) * ((210 : ℝ) - 130 * (1.61803395 : ℝ)) := by
 173      have : (1.4142 : ℝ) ≤ Real.sqrt 2 := hs2_lo
 174      have hcoeff_nonpos : ((210 : ℝ) - 130 * (1.61803395 : ℝ)) ≤ 0 := le_of_lt hcoeff_neg
 175      exact mul_le_mul_of_nonpos_right this hcoeff_nonpos
 176    have hnum :
 177        (348 : ℝ) - 204 * (1.61803395 : ℝ) + Real.sqrt 2 * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
 178          ≤ (348 : ℝ) - 204 * (1.61803395 : ℝ) + (1.4142 : ℝ) * ((210 : ℝ) - 130 * (1.61803395 : ℝ)) := by
 179      linarith
 180    have hrew1 :
 181        (348 : ℝ) - 204 * (1.61803395 : ℝ) + Real.sqrt 2 * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
 182          = (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ)) := by
 183      ring
 184    have hrew2 :
 185        (348 : ℝ) - 204 * (1.61803395 : ℝ) + (1.4142 : ℝ) * ((210 : ℝ) - 130 * (1.61803395 : ℝ))
 186          = (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) := by
 187      ring
 188    have hnum' :
 189        (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.61803395 : ℝ))
 190          ≤ (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) := by
 191      simpa [hrew1, hrew2] using hnum
 192    exact (div_le_div_of_nonneg_right hnum' (le_of_lt h7))
 193
 194  -- Combine the steps.
 195  have hw8_corner :
 196      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7
 197        ≤ (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) / 7 :=
 198    le_trans h_phi_step h_s2_step
 199
 200  -- Now the numeric corner value is < 2.490572090.
 201  have hcorner_lt :
 202      (348 + 210 * (1.4142 : ℝ) - (204 + 130 * (1.4142 : ℝ)) * (1.61803395 : ℝ)) / 7 < (2.490572090 : ℝ) := by
 203    norm_num
 204
 205  -- Finish by unfolding w8 and chaining inequalities.
 206  unfold IndisputableMonolith.Constants.w8_from_eight_tick
 207  exact lt_of_le_of_lt hw8_corner hcorner_lt
 208
 209/-- The gap weight interval for alphaInv bounds. -/
 210def w8Interval : Set ℝ :=
 211  Set.Icc (2490564399 / 1000000000 : ℝ) (2490572090 / 1000000000 : ℝ)
 212
 213end W8Bounds
 214end IndisputableMonolith.Numerics
 215