IndisputableMonolith.Numerics.Interval.AlphaBounds

   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.Log  -- [not in public release]
   4import IndisputableMonolith.Numerics.Interval.W8Bounds
   5import IndisputableMonolith.Constants.Alpha
   6
   7/-!
   8# Rigorous Bounds on α⁻¹ (Inverse Fine-Structure Constant)
   9
  10This module provides interval bounds on alphaInv using the symbolic derivation.
  11-/
  12
  13namespace IndisputableMonolith.Numerics
  14
  15open Interval
  16open Real (pi log)
  17open IndisputableMonolith.Constants (alphaInv alpha_seed f_gap w8_from_eight_tick)
  18
  19/-- alpha_seed = 4π·11 > 138.230048 -/
  20theorem alpha_seed_gt : (138.230048 : ℝ) < alpha_seed := by
  21  simp only [alpha_seed]
  22  have h := Real.pi_gt_d6
  23  linarith
  24
  25/-- alpha_seed = 4π·11 < 138.230092 -/
  26theorem alpha_seed_lt : alpha_seed < (138.230092 : ℝ) := by
  27  simp only [alpha_seed]
  28  have h := Real.pi_lt_d6
  29  linarith
  30
  31/-! ## f_gap bounds -/
  32
  33private def exp_taylor_10_at_048 : ℚ :=
  34  let x : ℚ := (48 : ℚ) / 100
  35  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
  36
  37private def exp_error_10_at_048 : ℚ :=
  38  let x : ℚ := (48 : ℚ) / 100
  39  x^10 * 11 / (Nat.factorial 10 * 10)
  40
  41private lemma exp_048_taylor_ceiling :
  42    exp_taylor_10_at_048 + exp_error_10_at_048 < (16161 / 10000 : ℚ) := by
  43  native_decide
  44
  45private lemma exp_048_lt : Real.exp (0.48 : ℝ) < (((16161 / 10000 : ℚ) : ℝ)) := by
  46  have hx_abs : |(0.48 : ℝ)| ≤ 1 := by norm_num
  47  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
  48  have h_abs := abs_sub_le_iff.mp h_bound
  49  have h_taylor_eq :
  50      (∑ m ∈ Finset.range 10, (0.48 : ℝ)^m / m.factorial) =
  51        (exp_taylor_10_at_048 : ℝ) := by
  52    simp only [exp_taylor_10_at_048, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
  53    norm_num
  54  have h_err_eq :
  55      |(0.48 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
  56        (exp_error_10_at_048 : ℝ) := by
  57    simp only [exp_error_10_at_048, Nat.factorial, Nat.succ_eq_add_one]
  58    norm_num
  59  have h_upper_raw :
  60      Real.exp (0.48 : ℝ) ≤
  61        |(0.48 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
  62          (exp_taylor_10_at_048 : ℝ) := by
  63    simpa [h_taylor_eq, add_comm, add_left_comm, add_assoc] using h_abs.1
  64  have h_upper :
  65      Real.exp (0.48 : ℝ) ≤ (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) := by
  66    calc
  67      Real.exp (0.48 : ℝ)
  68          ≤ |(0.48 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
  69              (exp_taylor_10_at_048 : ℝ) := h_upper_raw
  70      _ = (exp_error_10_at_048 : ℝ) + (exp_taylor_10_at_048 : ℝ) := by rw [h_err_eq]
  71      _ = (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) := by ring
  72  have h_num :
  73      (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) <
  74        (((16161 / 10000 : ℚ) : ℝ)) := by
  75    exact_mod_cast exp_048_taylor_ceiling
  76  exact lt_of_le_of_lt h_upper h_num
  77
  78private def exp_taylor_10_at_0481 : ℚ :=
  79  let x : ℚ := (481 : ℚ) / 1000
  80  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
  81
  82private def exp_error_10_at_0481 : ℚ :=
  83  let x : ℚ := (481 : ℚ) / 1000
  84  x^10 * 11 / (Nat.factorial 10 * 10)
  85
  86private lemma exp_0481_taylor_ceiling :
  87    exp_taylor_10_at_0481 + exp_error_10_at_0481 < (16177 / 10000 : ℚ) := by
  88  native_decide
  89
  90private lemma exp_0481_lt : Real.exp (0.481 : ℝ) < (((16177 / 10000 : ℚ) : ℝ)) := by
  91  have hx_abs : |(0.481 : ℝ)| ≤ 1 := by norm_num
  92  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
  93  have h_abs := abs_sub_le_iff.mp h_bound
  94  have h_taylor_eq :
  95      (∑ m ∈ Finset.range 10, (0.481 : ℝ)^m / m.factorial) =
  96        (exp_taylor_10_at_0481 : ℝ) := by
  97    simp only [exp_taylor_10_at_0481, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
  98    norm_num
  99  have h_err_eq :
 100      |(0.481 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
 101        (exp_error_10_at_0481 : ℝ) := by
 102    simp only [exp_error_10_at_0481, Nat.factorial, Nat.succ_eq_add_one]
 103    norm_num
 104  have h_upper_raw :
 105      Real.exp (0.481 : ℝ) ≤
 106        |(0.481 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
 107          (exp_taylor_10_at_0481 : ℝ) := by
 108    simpa [h_taylor_eq, add_comm, add_left_comm, add_assoc] using h_abs.1
 109  have h_upper :
 110      Real.exp (0.481 : ℝ) ≤ (exp_taylor_10_at_0481 : ℝ) + (exp_error_10_at_0481 : ℝ) := by
 111    calc
 112      Real.exp (0.481 : ℝ)
 113          ≤ |(0.481 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
 114              (exp_taylor_10_at_0481 : ℝ) := h_upper_raw
 115      _ = (exp_error_10_at_0481 : ℝ) + (exp_taylor_10_at_0481 : ℝ) := by rw [h_err_eq]
 116      _ = (exp_taylor_10_at_0481 : ℝ) + (exp_error_10_at_0481 : ℝ) := by ring
 117  have h_num :
 118      (exp_taylor_10_at_0481 : ℝ) + (exp_error_10_at_0481 : ℝ) <
 119        (((16177 / 10000 : ℚ) : ℝ)) := by
 120    exact_mod_cast exp_0481_taylor_ceiling
 121  exact lt_of_le_of_lt h_upper h_num
 122
 123private def exp_taylor_10_at_0483 : ℚ :=
 124  let x : ℚ := (483 : ℚ) / 1000
 125  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
 126
 127private def exp_error_10_at_0483 : ℚ :=
 128  let x : ℚ := (483 : ℚ) / 1000
 129  x^10 * 11 / (Nat.factorial 10 * 10)
 130
 131private lemma exp_0483_taylor_floor :
 132    (16209 / 10000 : ℚ) < exp_taylor_10_at_0483 - exp_error_10_at_0483 := by
 133  native_decide
 134
 135private lemma exp_0483_gt : (((16209 / 10000 : ℚ) : ℝ)) < Real.exp (0.483 : ℝ) := by
 136  have hx_abs : |(0.483 : ℝ)| ≤ 1 := by norm_num
 137  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
 138  have h_abs := abs_sub_le_iff.mp h_bound
 139  have h_taylor_eq :
 140      (∑ m ∈ Finset.range 10, (0.483 : ℝ)^m / m.factorial) =
 141        (exp_taylor_10_at_0483 : ℝ) := by
 142    simp only [exp_taylor_10_at_0483, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 143    norm_num
 144  have h_err_eq :
 145      |(0.483 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
 146        (exp_error_10_at_0483 : ℝ) := by
 147    simp only [exp_error_10_at_0483, Nat.factorial, Nat.succ_eq_add_one]
 148    norm_num
 149  have h_lower_raw :
 150      (exp_taylor_10_at_0483 : ℝ) ≤
 151        |(0.483 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
 152          Real.exp (0.483 : ℝ) := by
 153    simpa [h_taylor_eq, add_comm, add_left_comm, add_assoc] using h_abs.2
 154  have h_lower :
 155      (exp_taylor_10_at_0483 : ℝ) - (exp_error_10_at_0483 : ℝ) ≤ Real.exp (0.483 : ℝ) := by
 156    have h_lower' :
 157        (exp_taylor_10_at_0483 : ℝ) ≤ (exp_error_10_at_0483 : ℝ) + Real.exp (0.483 : ℝ) := by
 158      calc
 159        (exp_taylor_10_at_0483 : ℝ)
 160            ≤ |(0.483 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
 161                Real.exp (0.483 : ℝ) := h_lower_raw
 162        _ = (exp_error_10_at_0483 : ℝ) + Real.exp (0.483 : ℝ) := by rw [h_err_eq]
 163    linarith
 164  have h_num : (((16209 / 10000 : ℚ) : ℝ)) <
 165      (exp_taylor_10_at_0483 : ℝ) - (exp_error_10_at_0483 : ℝ) := by
 166    exact_mod_cast exp_0483_taylor_floor
 167  exact lt_of_lt_of_le h_num h_lower
 168
 169private lemma log_phi_gt_048 : (0.48 : ℝ) < log IndisputableMonolith.Constants.phi := by
 170  rw [Real.lt_log_iff_exp_lt IndisputableMonolith.Constants.phi_pos]
 171  have hphi_lo : (((16161 / 10000 : ℚ) : ℝ)) < IndisputableMonolith.Constants.phi := by
 172    have hphi : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := W8Bounds.phi_gt_161803395
 173    linarith
 174  exact lt_trans exp_048_lt hphi_lo
 175
 176private lemma log_phi_gt_0481 : (0.481 : ℝ) < log IndisputableMonolith.Constants.phi := by
 177  rw [Real.lt_log_iff_exp_lt IndisputableMonolith.Constants.phi_pos]
 178  have hphi_lo : (((16177 / 10000 : ℚ) : ℝ)) < IndisputableMonolith.Constants.phi := by
 179    have hphi : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := W8Bounds.phi_gt_161803395
 180    linarith
 181  exact lt_trans exp_0481_lt hphi_lo
 182
 183private lemma log_phi_lt_0483 : log IndisputableMonolith.Constants.phi < (0.483 : ℝ) := by
 184  rw [Real.log_lt_iff_lt_exp IndisputableMonolith.Constants.phi_pos]
 185  have hphi_hi : IndisputableMonolith.Constants.phi < (((16209 / 10000 : ℚ) : ℝ)) := by
 186    have hphi : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := W8Bounds.phi_lt_16180340
 187    linarith
 188  exact lt_trans hphi_hi exp_0483_gt
 189
 190theorem f_gap_gt : (1.195 : ℝ) < f_gap := by
 191  simp only [f_gap]
 192  have h_w8_lo := W8Bounds.w8_computed_gt
 193  have h_log_lo := log_phi_gt_048
 194  have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos
 195  have h048 : 0 < (0.48 : ℝ) := by norm_num
 196  -- f_gap = w8 * log(phi) > 2.490564399 * 0.48 = 1.19547...
 197  calc (1.195 : ℝ) < 2.490564399 * (0.48 : ℝ) := by norm_num
 198    _ < w8_from_eight_tick * (0.48 : ℝ) := by
 199      exact mul_lt_mul_of_pos_right h_w8_lo h048
 200    _ < w8_from_eight_tick * log IndisputableMonolith.Constants.phi := by
 201      exact mul_lt_mul_of_pos_left h_log_lo h_w8_pos
 202
 203/-- Stronger lower bound for the gap term using log(φ) > 0.481. -/
 204theorem f_gap_gt_strong : (1.1979 : ℝ) < f_gap := by
 205  simp only [f_gap]
 206  have h_w8_lo := W8Bounds.w8_computed_gt
 207  have h_log_lo := log_phi_gt_0481
 208  have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos
 209  have h0481 : 0 < (0.481 : ℝ) := by norm_num
 210  calc (1.1979 : ℝ) < 2.490564399 * (0.481 : ℝ) := by norm_num
 211    _ < w8_from_eight_tick * (0.481 : ℝ) := by
 212      exact mul_lt_mul_of_pos_right h_w8_lo h0481
 213    _ < w8_from_eight_tick * log IndisputableMonolith.Constants.phi := by
 214      exact mul_lt_mul_of_pos_left h_log_lo h_w8_pos
 215
 216theorem f_gap_lt : f_gap < (1.203 : ℝ) := by
 217  simp only [f_gap]
 218  have h_w8_hi := W8Bounds.w8_computed_lt
 219  have h_log_hi := log_phi_lt_0483
 220  have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos
 221  have h0483 : 0 < (0.483 : ℝ) := by norm_num
 222  -- f_gap = w8 * log(phi) < 2.490572090 * 0.483 = 1.202946...
 223  calc w8_from_eight_tick * log IndisputableMonolith.Constants.phi
 224      < w8_from_eight_tick * (0.483 : ℝ) := by
 225        exact mul_lt_mul_of_pos_left h_log_hi h_w8_pos
 226    _ < (2.490572090 : ℝ) * (0.483 : ℝ) := by
 227        exact mul_lt_mul_of_pos_right h_w8_hi h0483
 228    _ < (1.203 : ℝ) := by norm_num
 229
 230/-! ## Local exp bounds used by the exponential α formula -/
 231
 232private def exp_taylor_10_at_neg_00871 : ℚ :=
 233  let x : ℚ := -(871 : ℚ) / 100000
 234  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
 235
 236private def exp_error_10_at_neg_00871 : ℚ :=
 237  let x : ℚ := (871 : ℚ) / 100000
 238  x^10 * 11 / (Nat.factorial 10 * 10)
 239
 240private lemma exp_neg_00871_taylor_floor :
 241    (991327 / 1000000 : ℚ) < exp_taylor_10_at_neg_00871 - exp_error_10_at_neg_00871 := by
 242  native_decide
 243
 244private lemma exp_neg_00871_gt : ((991327 / 1000000 : ℚ) : ℝ) < Real.exp (-0.00871 : ℝ) := by
 245  have hx_abs : |(-0.00871 : ℝ)| ≤ 1 := by norm_num
 246  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
 247  have h_abs := abs_sub_le_iff.mp h_bound
 248  have h_taylor_eq :
 249      (∑ m ∈ Finset.range 10, (-0.00871 : ℝ)^m / m.factorial) =
 250        (exp_taylor_10_at_neg_00871 : ℝ) := by
 251    simp only [exp_taylor_10_at_neg_00871, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 252    norm_num
 253  have h_err_eq :
 254      |(-0.00871 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
 255        (exp_error_10_at_neg_00871 : ℝ) := by
 256    simp only [exp_error_10_at_neg_00871,
 257      Nat.factorial, Nat.succ_eq_add_one]
 258    norm_num
 259  have h_lower : (exp_taylor_10_at_neg_00871 : ℝ) - (exp_error_10_at_neg_00871 : ℝ) ≤ Real.exp (-0.00871 : ℝ) := by
 260    have h2 := h_abs.2
 261    simp only [h_taylor_eq] at h2
 262    linarith
 263  have h_num : ((991327 / 1000000 : ℚ) : ℝ) <
 264      (exp_taylor_10_at_neg_00871 : ℝ) - (exp_error_10_at_neg_00871 : ℝ) := by
 265    exact_mod_cast exp_neg_00871_taylor_floor
 266  exact lt_of_lt_of_le h_num h_lower
 267
 268private def exp_taylor_10_at_neg_00866 : ℚ :=
 269  let x : ℚ := -(866 : ℚ) / 100000
 270  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
 271
 272private def exp_error_10_at_neg_00866 : ℚ :=
 273  let x : ℚ := (866 : ℚ) / 100000
 274  x^10 * 11 / (Nat.factorial 10 * 10)
 275
 276private lemma exp_neg_00866_taylor_ceiling :
 277    exp_taylor_10_at_neg_00866 + exp_error_10_at_neg_00866 < (495689 / 500000 : ℚ) := by
 278  native_decide
 279
 280private lemma exp_neg_00866_lt : Real.exp (-0.00866 : ℝ) < ((495689 / 500000 : ℚ) : ℝ) := by
 281  have hx_abs : |(-0.00866 : ℝ)| ≤ 1 := by norm_num
 282  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
 283  have h_abs := abs_sub_le_iff.mp h_bound
 284  have h_taylor_eq :
 285      (∑ m ∈ Finset.range 10, (-0.00866 : ℝ)^m / m.factorial) =
 286        (exp_taylor_10_at_neg_00866 : ℝ) := by
 287    simp only [exp_taylor_10_at_neg_00866, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 288    norm_num
 289  have h_err_eq :
 290      |(-0.00866 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
 291        (exp_error_10_at_neg_00866 : ℝ) := by
 292    simp only [exp_error_10_at_neg_00866,
 293      Nat.factorial, Nat.succ_eq_add_one]
 294    norm_num
 295  have h_upper : Real.exp (-0.00866 : ℝ) ≤
 296      (exp_taylor_10_at_neg_00866 : ℝ) + (exp_error_10_at_neg_00866 : ℝ) := by
 297    have h1 := h_abs.1
 298    simp only [h_taylor_eq] at h1
 299    linarith
 300  have h_num : (exp_taylor_10_at_neg_00866 : ℝ) + (exp_error_10_at_neg_00866 : ℝ) <
 301      ((495689 / 500000 : ℚ) : ℝ) := by
 302    exact_mod_cast exp_neg_00866_taylor_ceiling
 303  exact lt_of_le_of_lt h_upper h_num
 304
 305/-! ## alphaInv bounds -/
 306
 307theorem alphaInv_gt : (137.030 : ℝ) < alphaInv := by
 308  simp only [alphaInv]
 309  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
 310  have hy_hi : f_gap / alpha_seed < (0.00871 : ℝ) := by
 311    have hmul : f_gap < (0.00871 : ℝ) * alpha_seed := by
 312      have h1 : f_gap < (1.203 : ℝ) := f_gap_lt
 313      have h2 : (1.203 : ℝ) < (0.00871 : ℝ) * (138.230048 : ℝ) := by norm_num
 314      have h3 : (0.00871 : ℝ) * (138.230048 : ℝ) < (0.00871 : ℝ) * alpha_seed := by
 315        exact mul_lt_mul_of_pos_left alpha_seed_gt (by norm_num)
 316      exact lt_trans h1 (lt_trans h2 h3)
 317    exact (div_lt_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
 318  have hexp_lo : ((991327 / 1000000 : ℚ) : ℝ) < Real.exp (-(f_gap / alpha_seed)) := by
 319    have hmono : Real.exp (-(0.00871 : ℝ)) < Real.exp (-(f_gap / alpha_seed)) := by
 320      exact Real.exp_lt_exp.mpr (by linarith [hy_hi])
 321    exact lt_trans exp_neg_00871_gt hmono
 322  have hseed_mul :
 323      (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ)) <
 324        alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) := by
 325    exact mul_lt_mul_of_pos_right alpha_seed_gt (by norm_num)
 326  have hmul :
 327      alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) <
 328        alpha_seed * Real.exp (-(f_gap / alpha_seed)) := by
 329    exact mul_lt_mul_of_pos_left hexp_lo hseed_pos
 330  calc
 331    (137.030 : ℝ) < (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := by norm_num
 332    _ < alpha_seed * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := hseed_mul
 333    _ < alpha_seed * Real.exp (-(f_gap / alpha_seed)) := hmul
 334
 335theorem alphaInv_lt : alphaInv < (137.039 : ℝ) := by
 336  simp only [alphaInv]
 337  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
 338  have hy_lo : (0.00866 : ℝ) < f_gap / alpha_seed := by
 339    have hmul : (0.00866 : ℝ) * alpha_seed < f_gap := by
 340      have h1 : (0.00866 : ℝ) * alpha_seed < (0.00866 : ℝ) * (138.230092 : ℝ) := by
 341        exact mul_lt_mul_of_pos_left alpha_seed_lt (by norm_num)
 342      have h2 : (0.00866 : ℝ) * (138.230092 : ℝ) < (1.1979 : ℝ) := by norm_num
 343      exact lt_trans h1 (lt_trans h2 f_gap_gt_strong)
 344    exact (lt_div_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
 345  have hexp_hi : Real.exp (-(f_gap / alpha_seed)) < ((495689 / 500000 : ℚ) : ℝ) := by
 346    have hmono : Real.exp (-(f_gap / alpha_seed)) < Real.exp (-(0.00866 : ℝ)) := by
 347      exact Real.exp_lt_exp.mpr (by linarith [hy_lo])
 348    exact lt_trans hmono exp_neg_00866_lt
 349  have hmul :
 350      alpha_seed * Real.exp (-(f_gap / alpha_seed)) <
 351        alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) := by
 352    exact mul_lt_mul_of_pos_left hexp_hi hseed_pos
 353  have hseed_hi :
 354      alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) <
 355        (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ)) := by
 356    exact mul_lt_mul_of_pos_right alpha_seed_lt (by norm_num)
 357  calc
 358    alpha_seed * Real.exp (-(f_gap / alpha_seed))
 359        < alpha_seed * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hmul
 360    _ < (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hseed_hi
 361    _ < (137.039 : ℝ) := by norm_num
 362
 363/-- Upper bound alias retained for backwards compatibility after the canonical
 364exponential α update. -/
 365theorem alphaInv_lt_strong : alphaInv < (137.039 : ℝ) := by
 366  exact alphaInv_lt
 367
 368end IndisputableMonolith.Numerics
 369