IndisputableMonolith.Physics.ElectronMass.Necessity

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.AlphaDerivation
   4import IndisputableMonolith.Constants.Alpha
   5import IndisputableMonolith.Physics.MassTopology
   6import IndisputableMonolith.Physics.ElectronMass.Defs
   7import IndisputableMonolith.RSBridge.Anchor
   8import IndisputableMonolith.Numerics.Interval.PhiBounds
   9import IndisputableMonolith.Numerics.Interval.AlphaBounds
  10import IndisputableMonolith.Numerics.Interval.Pow
  11import IndisputableMonolith.RSBridge.GapProperties
  12
  13/-!
  14# T9 Necessity: Electron Mass is Forced
  15
  16This module proves that the electron mass formula is **forced** from T8 (ledger
  17quantization) and the geometric constants derived in earlier theorems.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Physics
  22namespace ElectronMass
  23namespace Necessity
  24
  25open Real Constants AlphaDerivation MassTopology RSBridge
  26
  27/-! ## Part 1: Bounds on Constituent Constants -/
  28
  29/-- φ is bounded. We prove this directly using √5 bounds. -/
  30lemma phi_bounds : (1.618033 : ℝ) < phi ∧ phi < (1.618034 : ℝ) := by
  31  -- φ = (1 + √5)/2
  32  -- We need: 2.236066 < √5 < 2.236068
  33  have sqrt5_lower : (2.236066 : ℝ) < Real.sqrt 5 := by
  34    have h : (2.236066 : ℝ)^2 < 5 := by norm_num
  35    have h_pos : (0 : ℝ) ≤ 2.236066 := by norm_num
  36    rw [← Real.sqrt_sq h_pos]
  37    exact Real.sqrt_lt_sqrt (by norm_num) h
  38  have sqrt5_upper : Real.sqrt 5 < (2.236068 : ℝ) := by
  39    have h : (5 : ℝ) < 2.236068^2 := by norm_num
  40    have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
  41    have h_pos : (0 : ℝ) ≤ 2.236068 := by norm_num
  42    rw [← Real.sqrt_sq h_pos]
  43    exact Real.sqrt_lt_sqrt h5_pos h
  44  unfold phi
  45  constructor
  46  · -- Lower bound
  47    have h : (1.618033 : ℝ) = (1 + 2.236066) / 2 := by norm_num
  48    rw [h]
  49    apply div_lt_div_of_pos_right _ (by norm_num : (0 : ℝ) < 2)
  50    linarith
  51  · -- Upper bound
  52    have h : (1.618034 : ℝ) = (1 + 2.236068) / 2 := by norm_num
  53    rw [h]
  54    apply div_lt_div_of_pos_right _ (by norm_num : (0 : ℝ) < 2)
  55    linarith
  56
  57/-- Helper: Taylor sum for exp at x = 481211/1000000 (rational computation). -/
  58private def exp_taylor_10_at_481211 : ℚ :=
  59  let x : ℚ := 481211 / 1000000
  60  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
  61
  62/-- Helper: Error bound for 10-term Taylor at x = 481211/1000000. -/
  63private def exp_error_10_at_481211 : ℚ :=
  64  let x : ℚ := 481211 / 1000000
  65  x^10 * 11 / (Nat.factorial 10 * 10)
  66
  67/-- Combined: Taylor sum + error < 1.618033 -/
  68private lemma exp_combined_lt_target : exp_taylor_10_at_481211 + exp_error_10_at_481211 < 1618033 / 1000000 := by
  69  native_decide
  70
  71/-- The real Taylor sum equals the rational one -/
  72private lemma taylor_sum_eq_rational :
  73    1 + (0.481211 : ℝ) + 0.481211^2/2 + 0.481211^3/6 + 0.481211^4/24 +
  74    0.481211^5/120 + 0.481211^6/720 + 0.481211^7/5040 +
  75    0.481211^8/40320 + 0.481211^9/362880 = (exp_taylor_10_at_481211 : ℝ) := by
  76  simp only [exp_taylor_10_at_481211]
  77  norm_num
  78
  79/-- The real error term equals the rational one -/
  80private lemma error_term_eq_rational :
  81    (0.481211 : ℝ)^10 * (10 + 1) / (3628800 * 10) = (exp_error_10_at_481211 : ℝ) := by
  82  simp only [exp_error_10_at_481211, Nat.factorial]
  83  norm_num
  84
  85/-- The Taylor sum at 0.481211 is less than 1.618033 -/
  86private lemma taylor_sum_lt_target :
  87    1 + (0.481211 : ℝ) + 0.481211^2/2 + 0.481211^3/6 + 0.481211^4/24 +
  88    0.481211^5/120 + 0.481211^6/720 + 0.481211^7/5040 +
  89    0.481211^8/40320 + 0.481211^9/362880 +
  90    0.481211^10 * (10 + 1) / (3628800 * 10) < 1.618033 := by
  91  rw [taylor_sum_eq_rational, error_term_eq_rational]
  92  have h := exp_combined_lt_target
  93  have h_cast : (exp_taylor_10_at_481211 : ℝ) + (exp_error_10_at_481211 : ℝ) <
  94                ((1618033 : ℚ) / 1000000 : ℝ) := by exact_mod_cast h
  95  calc (exp_taylor_10_at_481211 : ℝ) + (exp_error_10_at_481211 : ℝ)
  96      < ((1618033 : ℚ) / 1000000 : ℝ) := h_cast
  97    _ = (1.618033 : ℝ) := by norm_num
  98
  99/-- log(1.618033) > 0.481211 -/
 100theorem log_lower_numerical : (0.481211 : ℝ) < Real.log (1.618033 : ℝ) := by
 101  rw [Real.lt_log_iff_exp_lt (by norm_num : (0 : ℝ) < 1.618033)]
 102  have hx_pos : (0 : ℝ) ≤ (0.481211 : ℝ) := by norm_num
 103  have hx_le1 : (0.481211 : ℝ) ≤ 1 := by norm_num
 104  have h_bound := Real.exp_bound' hx_pos hx_le1 (n := 10) (by norm_num : 0 < 10)
 105  calc Real.exp (0.481211 : ℝ)
 106      ≤ (1 + 0.481211 + 0.481211^2/2 + 0.481211^3/6 + 0.481211^4/24 +
 107         0.481211^5/120 + 0.481211^6/720 + 0.481211^7/5040 +
 108         0.481211^8/40320 + 0.481211^9/362880) +
 109        0.481211^10 * (10 + 1) / (Nat.factorial 10 * 10) := by
 110          simpa [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial] using h_bound
 111    _ = 1 + 0.481211 + 0.481211^2/2 + 0.481211^3/6 + 0.481211^4/24 +
 112        0.481211^5/120 + 0.481211^6/720 + 0.481211^7/5040 +
 113        0.481211^8/40320 + 0.481211^9/362880 +
 114        0.481211^10 * (10 + 1) / (3628800 * 10) := by
 115          simp only [Nat.factorial]; norm_num
 116    _ < 1.618033 := taylor_sum_lt_target
 117
 118/-- Taylor sum for exp at x = 481212/1000000 -/
 119private def exp_taylor_10_at_481212 : ℚ :=
 120  let x : ℚ := 481212 / 1000000
 121  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
 122
 123/-- Error bound for 10-term Taylor at x = 481212/1000000 -/
 124private def exp_error_10_at_481212 : ℚ :=
 125  let x : ℚ := 481212 / 1000000
 126  x^10 * 11 / (Nat.factorial 10 * 10)
 127
 128/-- The Taylor sum at 0.481212 is greater than 1.618034 + error -/
 129private lemma exp_taylor_481212_gt_target :
 130    1618034 / 1000000 + exp_error_10_at_481212 < exp_taylor_10_at_481212 := by
 131  native_decide
 132
 133/-- log(1.618034) < 0.481212 -/
 134theorem log_upper_numerical : Real.log (1.618034 : ℝ) < (0.481212 : ℝ) := by
 135  rw [Real.log_lt_iff_lt_exp (by norm_num : (0 : ℝ) < 1.618034)]
 136  have hx_abs : |(0.481212 : ℝ)| ≤ 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_gt := exp_taylor_481212_gt_target
 140  have h_cast : ((1618034 : ℚ) / 1000000 : ℝ) + (exp_error_10_at_481212 : ℝ) <
 141                (exp_taylor_10_at_481212 : ℝ) := by exact_mod_cast h_taylor_gt
 142  have h_sum_eq : (∑ m ∈ Finset.range 10, (0.481212 : ℝ)^m / m.factorial) =
 143      (exp_taylor_10_at_481212 : ℝ) := by
 144    simp only [exp_taylor_10_at_481212, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 145    norm_num
 146  have h_err_eq : |(0.481212 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
 147      (exp_error_10_at_481212 : ℝ) := by
 148    simp only [abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.481212), exp_error_10_at_481212,
 149               Nat.factorial, Nat.succ_eq_add_one]
 150    norm_num
 151  have h_lower : (exp_taylor_10_at_481212 : ℝ) - (exp_error_10_at_481212 : ℝ) ≤
 152                 Real.exp (0.481212 : ℝ) := by
 153    have h2 := h_abs.2
 154    simp only [h_sum_eq, h_err_eq] at h2
 155    linarith
 156  calc (1.618034 : ℝ)
 157      = ((1618034 : ℚ) / 1000000 : ℝ) := by norm_num
 158    _ < (exp_taylor_10_at_481212 : ℝ) - (exp_error_10_at_481212 : ℝ) := by linarith [h_cast]
 159    _ ≤ Real.exp (0.481212 : ℝ) := h_lower
 160
 161/-- log(φ) is bounded. -/
 162lemma log_phi_bounds : (0.481211 : ℝ) < Real.log phi ∧ Real.log phi < (0.481212 : ℝ) := by
 163  have hphi := phi_bounds
 164  have h_phi_pos : 0 < phi := phi_pos
 165  have h_low_pos : (0 : ℝ) < 1.618033 := by norm_num
 166  have h_log_lower : Real.log (1.618033 : ℝ) < Real.log phi :=
 167    Real.log_lt_log h_low_pos hphi.1
 168  have h_log_upper : Real.log phi < Real.log (1.618034 : ℝ) :=
 169    Real.log_lt_log h_phi_pos hphi.2
 170  constructor
 171  · exact lt_trans log_lower_numerical h_log_lower
 172  · exact lt_trans h_log_upper log_upper_numerical
 173
 174/-- α is bounded. -/
 175lemma alpha_bounds : (0.007297 : ℝ) < alpha ∧ alpha < (0.0072977 : ℝ) := by
 176  have h_lower := IndisputableMonolith.Numerics.alphaInv_gt
 177  have h_upper := IndisputableMonolith.Numerics.alphaInv_lt
 178  have h_pos : 0 < alphaInv := lt_trans (by norm_num : (0 : ℝ) < 137.030) h_lower
 179  simp only [alpha]
 180  constructor
 181  · have h1 : alphaInv < 1 / 0.007297 := calc
 182      alphaInv < 137.039 := h_upper
 183      _ < 1 / 0.007297 := by norm_num
 184    have h_inv_bound : 1 / (1 / 0.007297) < 1 / alphaInv := by
 185      apply one_div_lt_one_div_of_lt h_pos h1
 186    simp only [one_div_one_div] at h_inv_bound
 187    exact h_inv_bound
 188  · have h2 : 1 / 0.0072977 < alphaInv := calc
 189      1 / 0.0072977 < 137.030 := by norm_num
 190      _ < alphaInv := h_lower
 191    have h_denom_pos : (0 : ℝ) < 1 / 0.0072977 := by norm_num
 192    have h_inv_bound : 1 / alphaInv < 1 / (1 / 0.0072977) := by
 193      apply one_div_lt_one_div_of_lt h_denom_pos h2
 194    simp only [one_div_one_div] at h_inv_bound
 195    exact h_inv_bound
 196
 197/-- α² is bounded. -/
 198lemma alpha_sq_bounds : (0.0000532 : ℝ) < alpha^2 ∧ alpha^2 < (0.0000533 : ℝ) := by
 199  have h := alpha_bounds
 200  constructor
 201  · have h1 : (0.007297 : ℝ)^2 < alpha^2 := sq_lt_sq' (by linarith) h.1
 202    calc (0.0000532 : ℝ) < 0.007297^2 := by norm_num
 203      _ < alpha^2 := h1
 204  · have h2 : alpha^2 < (0.0072977 : ℝ)^2 := sq_lt_sq' (by linarith) h.2
 205    calc alpha^2 < 0.0072977^2 := h2
 206      _ < (0.0000533 : ℝ) := by norm_num
 207
 208/-- α³ is bounded. -/
 209lemma alpha_cube_bounds : (0.000000388 : ℝ) < alpha^3 ∧ alpha^3 < (0.000000389 : ℝ) := by
 210  have h := alpha_bounds
 211  constructor
 212  · have h1 : (0.007297 : ℝ)^3 < alpha^3 := by
 213      have : (0.007297 : ℝ) < alpha := h.1
 214      nlinarith [sq_nonneg alpha, sq_nonneg (0.007297 : ℝ)]
 215    calc (0.000000388 : ℝ) < 0.007297^3 := by norm_num
 216      _ < alpha^3 := h1
 217  · have h2 : alpha^3 < (0.0072977 : ℝ)^3 := by
 218      have : alpha < (0.0072977 : ℝ) := h.2
 219      nlinarith [sq_nonneg alpha, sq_nonneg (0.0072977 : ℝ)]
 220    calc alpha^3 < 0.0072977^3 := h2
 221      _ < (0.000000389 : ℝ) := by norm_num
 222
 223/-! ## Part 2: Bounds on Derived Quantities -/
 224
 225lemma ledger_fraction_exact : (ledger_fraction : ℝ) = 29 / 44 := by
 226  simp only [ledger_fraction, W, E_total, E_passive, wallpaper_groups, cube_edges, passive_field_edges, active_edges_per_tick]
 227  norm_num
 228
 229lemma base_shift_bounds : (34.6590 : ℝ) < base_shift ∧ base_shift < (34.6592 : ℝ) := by
 230  simp only [base_shift, W, wallpaper_groups]
 231  rw [ledger_fraction_exact]
 232  norm_num
 233
 234lemma radiative_correction_bounds :
 235    (0.0000578 : ℝ) < radiative_correction ∧ radiative_correction < (0.0000580 : ℝ) := by
 236  simp only [radiative_correction, correction_order_2, correction_order_3, E_total, cube_edges]
 237  have h2 := alpha_sq_bounds
 238  have h3 := alpha_cube_bounds
 239  constructor <;> linarith
 240
 241lemma refined_shift_bounds :
 242    (34.6590 : ℝ) < refined_shift ∧ refined_shift < (34.6593 : ℝ) := by
 243  simp only [refined_shift]
 244  have hb := base_shift_bounds
 245  have hr := radiative_correction_bounds
 246  constructor <;> linarith
 247
 248/-! ## Part 3: Bounds on Gap Function -/
 249
 250/-- Z value for the electron: 1332. -/
 251lemma electron_Z_value : ZOf Fermion.e = 1332 := by
 252  simp only [ZOf, tildeQ, sectorOf]
 253  norm_num
 254
 255/-- Hypothesis: exp(6.7144) < 824.2 -/
 256def exp_67144_lt_824_hypothesis : Prop := Real.exp (6.7144 : ℝ) < (824.2 : ℝ)
 257
 258/-- Hypothesis: 824.2218 < exp(6.7145) -/
 259def val_824_lt_exp_67145_hypothesis : Prop := (824.2218 : ℝ) < Real.exp (6.7145 : ℝ)
 260
 261/-!
 262Rigorous closure of the two exp endpoint hypotheses:
 263
 264- `exp(6.7144) < 824.2`
 265- `824.2218 < exp(6.7145)`
 266
 267Proof strategy:
 2681. Split `exp(6 + x) = exp(6) * exp(x)`.
 2692. Bound `exp(6)` via `exp(1)` bounds (`Real.exp_one_gt_d9`, `Real.exp_one_lt_d9`) and `Real.exp_nat_mul`.
 2703. Bound `exp(0.7144)`/`exp(0.7145)` via 10-term Taylor bounds (`Real.exp_bound'` / `Real.exp_bound`) with exact rational checks (`native_decide`).
 271-/
 272
 273private lemma exp_six_upper : Real.exp (6 : ℝ) < (403.428794 : ℝ) := by
 274  have hpow : (Real.exp (1 : ℝ)) ^ (6 : ℕ) ≤ (2.7182818286 : ℝ) ^ (6 : ℕ) := by
 275    exact pow_le_pow_left₀ (Real.exp_pos (1 : ℝ)).le (Real.exp_one_lt_d9).le 6
 276  have hnum : (2.7182818286 : ℝ) ^ (6 : ℕ) < (403.428794 : ℝ) := by norm_num
 277  have hEq : Real.exp (6 : ℝ) = (Real.exp (1 : ℝ)) ^ (6 : ℕ) := by
 278    calc
 279      Real.exp (6 : ℝ) = Real.exp ((6 : ℕ) * (1 : ℝ)) := by norm_num
 280      _ = (Real.exp (1 : ℝ)) ^ (6 : ℕ) := by simpa using (Real.exp_nat_mul (1 : ℝ) 6)
 281  rw [hEq]
 282  exact lt_of_le_of_lt hpow hnum
 283
 284private lemma exp_six_lower : (403.428793 : ℝ) < Real.exp (6 : ℝ) := by
 285  have hpow : (2.7182818283 : ℝ) ^ (6 : ℕ) < (Real.exp (1 : ℝ)) ^ (6 : ℕ) := by
 286    exact pow_lt_pow_left₀ Real.exp_one_gt_d9 (by norm_num) (by norm_num : (6 : ℕ) ≠ 0)
 287  have hnum : (403.428793 : ℝ) < (2.7182818283 : ℝ) ^ (6 : ℕ) := by norm_num
 288  have hEq : Real.exp (6 : ℝ) = (Real.exp (1 : ℝ)) ^ (6 : ℕ) := by
 289    calc
 290      Real.exp (6 : ℝ) = Real.exp ((6 : ℕ) * (1 : ℝ)) := by norm_num
 291      _ = (Real.exp (1 : ℝ)) ^ (6 : ℕ) := by simpa using (Real.exp_nat_mul (1 : ℝ) 6)
 292  have hpow' : (2.7182818283 : ℝ) ^ (6 : ℕ) < Real.exp (6 : ℝ) := by
 293    rw [hEq]
 294    exact hpow
 295  exact lt_trans hnum hpow'
 296
 297/-- Taylor sum for exp at x = 7144/10000. -/
 298private def exp_taylor_10_at_7144 : ℚ :=
 299  let x : ℚ := 7144 / 10000
 300  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
 301
 302/-- Error bound for 10-term Taylor at x = 7144/10000. -/
 303private def exp_error_10_at_7144 : ℚ :=
 304  let x : ℚ := 7144 / 10000
 305  x^10 * 11 / (Nat.factorial 10 * 10)
 306
 307private lemma exp_07144_upper_q :
 308    exp_taylor_10_at_7144 + exp_error_10_at_7144 < 2042961 / 1000000 := by
 309  native_decide
 310
 311private lemma exp_07144_upper : Real.exp (0.7144 : ℝ) < (2.042961 : ℝ) := by
 312  have hx_pos : (0 : ℝ) ≤ (0.7144 : ℝ) := by norm_num
 313  have hx_le1 : (0.7144 : ℝ) ≤ 1 := by norm_num
 314  have h_bound := Real.exp_bound' hx_pos hx_le1 (n := 10) (by norm_num : 0 < 10)
 315  have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.7144 : ℝ)^m / m.factorial) =
 316      (exp_taylor_10_at_7144 : ℝ) := by
 317    simp only [exp_taylor_10_at_7144, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 318    norm_num
 319  have h_err_eq : (0.7144 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) =
 320      (exp_error_10_at_7144 : ℝ) := by
 321    simp only [exp_error_10_at_7144, Nat.factorial]
 322    norm_num
 323  have h_cast : (exp_taylor_10_at_7144 : ℝ) + (exp_error_10_at_7144 : ℝ) <
 324      ((2042961 : ℚ) / 1000000 : ℝ) := by
 325    exact_mod_cast exp_07144_upper_q
 326  calc Real.exp (0.7144 : ℝ)
 327      ≤ (∑ m ∈ Finset.range 10, (0.7144 : ℝ)^m / m.factorial) +
 328        (0.7144 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) := h_bound
 329    _ = (exp_taylor_10_at_7144 : ℝ) + (exp_error_10_at_7144 : ℝ) := by rw [h_taylor_eq, h_err_eq]
 330    _ < ((2042961 : ℚ) / 1000000 : ℝ) := h_cast
 331    _ = (2.042961 : ℝ) := by norm_num
 332
 333/-- Taylor sum for exp at x = 7145/10000. -/
 334private def exp_taylor_10_at_7145 : ℚ :=
 335  let x : ℚ := 7145 / 10000
 336  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
 337
 338/-- Error bound for 10-term Taylor at x = 7145/10000. -/
 339private def exp_error_10_at_7145 : ℚ :=
 340  let x : ℚ := 7145 / 10000
 341  x^10 * 11 / (Nat.factorial 10 * 10)
 342
 343private lemma exp_07145_lower_q :
 344    20431648 / 10000000 + exp_error_10_at_7145 < exp_taylor_10_at_7145 := by
 345  native_decide
 346
 347private lemma exp_07145_lower : (2.0431648 : ℝ) < Real.exp (0.7145 : ℝ) := by
 348  have hx_abs : |(0.7145 : ℝ)| ≤ 1 := by norm_num
 349  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
 350  have h_abs := abs_sub_le_iff.mp h_bound
 351  have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.7145 : ℝ)^m / m.factorial) =
 352      (exp_taylor_10_at_7145 : ℝ) := by
 353    simp only [exp_taylor_10_at_7145, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 354    norm_num
 355  have h_err_eq : |(0.7145 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
 356      (exp_error_10_at_7145 : ℝ) := by
 357    simp only [abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.7145), exp_error_10_at_7145,
 358      Nat.factorial, Nat.succ_eq_add_one]
 359    norm_num
 360  have h_cast : ((20431648 : ℚ) / 10000000 : ℝ) + (exp_error_10_at_7145 : ℝ) <
 361      (exp_taylor_10_at_7145 : ℝ) := by
 362    exact_mod_cast exp_07145_lower_q
 363  have h_lower : (exp_taylor_10_at_7145 : ℝ) - (exp_error_10_at_7145 : ℝ) ≤
 364      Real.exp (0.7145 : ℝ) := by
 365    have h2 := h_abs.2
 366    simp only [h_taylor_eq, h_err_eq] at h2
 367    linarith
 368  calc (2.0431648 : ℝ) = ((20431648 : ℚ) / 10000000 : ℝ) := by norm_num
 369    _ < (exp_taylor_10_at_7145 : ℝ) - (exp_error_10_at_7145 : ℝ) := by linarith [h_cast]
 370    _ ≤ Real.exp (0.7145 : ℝ) := h_lower
 371
 372theorem exp_67144_lt_824 : exp_67144_lt_824_hypothesis := by
 373  unfold exp_67144_lt_824_hypothesis
 374  have hsplit : Real.exp (6.7144 : ℝ) = Real.exp (6 : ℝ) * Real.exp (0.7144 : ℝ) := by
 375    have h : (6.7144 : ℝ) = (6 : ℝ) + 0.7144 := by norm_num
 376    rw [h, Real.exp_add]
 377  rw [hsplit]
 378  have h6 := exp_six_upper
 379  have hfrac := exp_07144_upper
 380  have hprod : Real.exp (6 : ℝ) * Real.exp (0.7144 : ℝ) < (403.428794 : ℝ) * (2.042961 : ℝ) := by
 381    nlinarith [h6, hfrac, Real.exp_pos (6 : ℝ), Real.exp_pos (0.7144 : ℝ)]
 382  have hnum : (403.428794 : ℝ) * (2.042961 : ℝ) < (824.2 : ℝ) := by norm_num
 383  exact lt_trans hprod hnum
 384
 385theorem val_824_lt_exp_67145 : val_824_lt_exp_67145_hypothesis := by
 386  unfold val_824_lt_exp_67145_hypothesis
 387  have hsplit : Real.exp (6.7145 : ℝ) = Real.exp (6 : ℝ) * Real.exp (0.7145 : ℝ) := by
 388    have h : (6.7145 : ℝ) = (6 : ℝ) + 0.7145 := by norm_num
 389    rw [h, Real.exp_add]
 390  rw [hsplit]
 391  have h6 := exp_six_lower
 392  have hfrac := exp_07145_lower
 393  have hprod : (403.428793 : ℝ) * (2.0431648 : ℝ) < Real.exp (6 : ℝ) * Real.exp (0.7145 : ℝ) := by
 394    nlinarith [h6, hfrac, Real.exp_pos (6 : ℝ), Real.exp_pos (0.7145 : ℝ)]
 395  have hnum : (824.2218 : ℝ) < (403.428793 : ℝ) * (2.0431648 : ℝ) := by norm_num
 396  exact lt_trans hnum hprod
 397
 398theorem one_plus_1332_div_phi_lower : (824.2 : ℝ) < 1 + 1332 / (1.618034 : ℝ) := by
 399  have h_pos : (0 : ℝ) < 1.618034 := by norm_num
 400  have h_key : (1.618034 : ℝ) * 823.2 < 1332 := by nlinarith
 401  have h_ineq : (823.2 : ℝ) < 1332 / 1.618034 := by
 402    rw [lt_div_iff₀' h_pos]
 403    exact h_key
 404  linarith
 405
 406theorem log_824_lower :
 407    (6.7144 : ℝ) < Real.log (1 + 1332 / (1.618034 : ℝ)) := by
 408  have h_pos : (0 : ℝ) < 1 + 1332 / 1.618034 := by positivity
 409  rw [Real.lt_log_iff_exp_lt h_pos]
 410  calc Real.exp 6.7144 < 824.2 := exp_67144_lt_824
 411    _ < 1 + 1332 / 1.618034 := one_plus_1332_div_phi_lower
 412
 413theorem one_plus_1332_div_phi_upper : 1 + 1332 / (1.618033 : ℝ) < (824.2218 : ℝ) := by
 414  have h_pos : (0 : ℝ) < 1.618033 := by norm_num
 415  have h_key : (1332 : ℝ) < 823.2218 * 1.618033 := by nlinarith
 416  have h_ineq : 1332 / (1.618033 : ℝ) < 823.2218 := by
 417    rw [div_lt_iff₀ h_pos]
 418    exact h_key
 419  linarith
 420
 421theorem log_824_upper :
 422    Real.log (1 + 1332 / (1.618033 : ℝ)) < (6.7145 : ℝ) := by
 423  have h_pos : (0 : ℝ) < 1 + 1332 / 1.618033 := by positivity
 424  rw [Real.log_lt_iff_lt_exp h_pos]
 425  calc 1 + 1332 / 1.618033 < 824.2218 := one_plus_1332_div_phi_upper
 426    _ < Real.exp 6.7145 := val_824_lt_exp_67145
 427
 428lemma gap_1332_bounds :
 429    (13.953 : ℝ) < gap 1332 ∧ gap 1332 < (13.954 : ℝ) := by
 430  simp only [gap]
 431  have hphi := phi_bounds
 432  have h_phi_pos : (0 : ℝ) < phi := by linarith [hphi.1]
 433  -- Use the local, proven `log_phi_bounds` in this module (no external hypotheses needed).
 434  have hlog := log_phi_bounds
 435  have h_log_pos : 0 < Real.log phi := Real.log_pos (by linarith [hphi.1])
 436  have h_log_lower : (6.7144 : ℝ) < Real.log (1 + 1332 / phi) := by
 437    have h_arg : 1 + 1332 / (1.618034 : ℝ) < 1 + 1332 / phi := by
 438      have ha : (0 : ℝ) < (1332 : ℝ) := by norm_num
 439      exact add_lt_add_right (div_lt_div_of_pos_left ha h_phi_pos hphi.2) 1
 440    exact lt_trans log_824_lower (Real.log_lt_log (by norm_num) h_arg)
 441  have h_log_upper : Real.log (1 + 1332 / phi) < (6.7145 : ℝ) := by
 442    have h_arg : 1 + 1332 / phi < 1 + 1332 / (1.618033 : ℝ) := by
 443      have ha : (0 : ℝ) < (1332 : ℝ) := by norm_num
 444      have hc : (0 : ℝ) < (1.618033 : ℝ) := by norm_num
 445      exact add_lt_add_right (div_lt_div_of_pos_left ha hc hphi.1) 1
 446    have h_pos : (0 : ℝ) < 1 + 1332 / phi := by
 447      have h_div_pos : (0 : ℝ) < (1332 : ℝ) / phi := div_pos (by norm_num) h_phi_pos
 448      linarith
 449    exact lt_trans (Real.log_lt_log h_pos h_arg) log_824_upper
 450  constructor
 451  · have h_chain : 13.953 * Real.log phi < Real.log (1 + 1332 / phi) := by
 452      have h1 : 13.953 * Real.log phi < 13.953 * 0.481212 := by nlinarith [hlog.2]
 453      linarith
 454    exact (lt_div_iff₀ h_log_pos).mpr h_chain
 455  · have h_chain : Real.log (1 + 1332 / phi) < 13.954 * Real.log phi := by
 456      have h1 : 13.954 * 0.481211 < 13.954 * Real.log phi := by nlinarith [hlog.1]
 457      linarith
 458    exact (div_lt_iff₀ h_log_pos).mpr h_chain
 459
 460/-! ## Part 4: The Main Bounds -/
 461
 462/-- **PROVEN**: Tight bounds on the structural mass scale.
 463
 464This is a purely geometric constant:
 465`electron_structural_mass = 2^(-22) * φ^51`.
 466
 467We bound `φ^51` using Fibonacci identities and tight rational bounds from
 468`Numerics/Interval/PhiBounds.lean`, then divide by `2^22 = 4194304`.
 469
 470This lemma is used downstream in the neutrino and quark mass checks. -/
 471theorem structural_mass_bounds :
 472    (10856 : ℝ) < IndisputableMonolith.Physics.ElectronMass.electron_structural_mass ∧
 473      IndisputableMonolith.Physics.ElectronMass.electron_structural_mass < (10858 : ℝ) := by
 474  -- Rewrite to the closed form `2^(-22) * φ^51`.
 475  have h_forced := IndisputableMonolith.Physics.ElectronMass.electron_structural_mass_forced
 476  -- `Constants.phi` is definitionally `Real.goldenRatio` in this project.
 477  have hphi : (phi : ℝ) = Real.goldenRatio := rfl
 478  -- Evaluate `2^22`.
 479  have h2pow : (2 : ℝ) ^ (22 : ℕ) = (4194304 : ℝ) := by norm_num
 480  -- Convert `2^(-22 : ℤ)` to `1 / 4194304`.
 481  have h2neg : (2 : ℝ) ^ (-22 : ℤ) = (1 : ℝ) / (4194304 : ℝ) := by
 482    -- `2 ^ (-22) = (2 ^ 22)⁻¹ = 1 / (2 ^ 22)`.
 483    have h2_ne : (2 : ℝ) ≠ 0 := by norm_num
 484    calc
 485      (2 : ℝ) ^ (-22 : ℤ)
 486          = ((2 : ℝ) ^ (22 : ℤ))⁻¹ := by
 487              -- `a^(-n) = (a^n)⁻¹`
 488              simpa using (zpow_neg (2 : ℝ) (22 : ℤ))
 489      _   = ((2 : ℝ) ^ (22 : ℕ))⁻¹ := by
 490              -- coerce positive exponent back to Nat power
 491              simp [zpow_ofNat]
 492      _   = ((4194304 : ℝ))⁻¹ := by
 493              simpa [h2pow]
 494      _   = (1 : ℝ) / (4194304 : ℝ) := by
 495              -- avoid simp looping between `inv_eq_one_div` and `one_div`
 496              exact (inv_eq_one_div (4194304 : ℝ))
 497  -- Convert `φ^(51 : ℤ)` to `φ^51` and rewrite `φ` to `goldenRatio`.
 498  have hphi51 : (phi : ℝ) ^ (51 : ℤ) = Real.goldenRatio ^ (51 : ℕ) := by
 499    -- `zpow_ofNat` + definitional `phi = goldenRatio`
 500    simpa [hphi, zpow_ofNat]
 501  -- Now bound using the proven interval for `goldenRatio^51`.
 502  have h51_lo := IndisputableMonolith.Numerics.phi_pow51_gt
 503  have h51_hi := IndisputableMonolith.Numerics.phi_pow51_lt
 504  -- Assemble the value.
 505  -- electron_structural_mass = (1/4194304) * goldenRatio^51
 506  have hm :
 507      IndisputableMonolith.Physics.ElectronMass.electron_structural_mass
 508        = (1 : ℝ) / (4194304 : ℝ) * (Real.goldenRatio ^ (51 : ℕ)) := by
 509    -- Start from the forced form.
 510    rw [h_forced]
 511    -- Replace `2^(-22)` and `φ^(51:ℤ)`.
 512    simp [h2neg, hphi51]
 513  -- Divide the `φ^51` interval by 2^22 to get the desired numeric bounds.
 514  have hden_pos : (0 : ℝ) < (4194304 : ℝ) := by norm_num
 515  constructor
 516  · -- lower bound
 517    -- Use a coarse numerical inequality: 10856 < (45537548334 / 4194304)
 518    have h_coarse : (10856 : ℝ) < (45537548334 : ℝ) / (4194304 : ℝ) := by
 519      norm_num
 520    -- From h51_lo: 45537548334 < φ^51, so dividing by positive denom preserves inequality.
 521    have h_div : (45537548334 : ℝ) / (4194304 : ℝ) < (Real.goldenRatio ^ (51 : ℕ)) / (4194304 : ℝ) :=
 522      (div_lt_div_of_pos_right h51_lo hden_pos)
 523    -- Convert to the exact form in `hm`.
 524    -- Note: (1/den) * x = x/den
 525    have h_form : (1 : ℝ) / (4194304 : ℝ) * (Real.goldenRatio ^ (51 : ℕ))
 526        = (Real.goldenRatio ^ (51 : ℕ)) / (4194304 : ℝ) := by
 527      have hne : (4194304 : ℝ) ≠ 0 := by norm_num
 528      field_simp [hne]
 529    -- Chain inequalities.
 530    rw [hm, h_form]
 531    exact lt_trans h_coarse h_div
 532  · -- upper bound
 533    -- Use a coarse numerical inequality: (45537549354 / 4194304) < 10858
 534    have h_coarse : (45537549354 : ℝ) / (4194304 : ℝ) < (10858 : ℝ) := by
 535      norm_num
 536    -- From h51_hi: φ^51 < 45537549354, divide by positive denom.
 537    have h_div : (Real.goldenRatio ^ (51 : ℕ)) / (4194304 : ℝ) < (45537549354 : ℝ) / (4194304 : ℝ) :=
 538      (div_lt_div_of_pos_right h51_hi hden_pos)
 539    have h_form : (1 : ℝ) / (4194304 : ℝ) * (Real.goldenRatio ^ (51 : ℕ))
 540        = (Real.goldenRatio ^ (51 : ℕ)) / (4194304 : ℝ) := by
 541      have hne : (4194304 : ℝ) ≠ 0 := by norm_num
 542      field_simp [hne]
 543    rw [hm, h_form]
 544    exact lt_trans h_div h_coarse
 545
 546/-- Hypothesis: electron_residue > -20.7063 -/
 547def electron_residue_lower_hypothesis : Prop := (-20.7063 : ℝ) < IndisputableMonolith.Physics.ElectronMass.electron_residue
 548
 549/-- Hypothesis: electron_residue < -20.7057 -/
 550def electron_residue_upper_hypothesis : Prop := IndisputableMonolith.Physics.ElectronMass.electron_residue < (-20.7057 : ℝ)
 551
 552/-- Hypothesis: φ^(-20.7063) > 4.705e-5 -/
 553def phi_pow_neg207063_lower_hypothesis : Prop := (4.705e-5 : ℝ) < phi ^ (-20.7063 : ℝ)
 554
 555/-- Hypothesis: φ^(-20.705) < 4.709e-5 -/
 556def phi_pow_neg20705_upper_hypothesis : Prop := phi ^ (-20.705 : ℝ) < (4709 / 100000000 : ℝ)
 557
 558end Necessity
 559end ElectronMass
 560end Physics
 561end IndisputableMonolith
 562