IndisputableMonolith.Physics.ElectronGMinus2ScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants.Alpha
   3import IndisputableMonolith.Numerics.Interval.AlphaBounds
   4
   5/-!
   6# Electron g-2 Score Card
   7
   8Phase 1 row **P1-C05** in `planning/PHYSICAL_DERIVATION_PLAN.md`.
   9
  10## Statement
  11
  12The theorem-grade slice is the leading Schwinger term
  13
  14`a_e^(1) = α / (2π)`.
  15
  16Using the certified RS `alphaInv` interval, this module proves
  17
  18`0.001161 < a_e^(1) < 0.001162`.
  19
  20The CODATA electron anomaly is
  21
  22`a_e = 0.00115965218059...`.
  23
  24The leading term alone is within `0.3%` of CODATA, but the full electron
  25g-2 row remains **PARTIAL_THEOREM** because the higher-order loop series
  26has not yet been derived from RS primitives in this module.
  27
  28Falsifier: CODATA `a_e` outside the stated residual band for the
  29Schwinger-only slice, or failure to derive the missing loop terms from
  30the RS/QED bridge.
  31
  32## Lean status: 0 sorry, 0 axiom
  33-/
  34
  35namespace IndisputableMonolith.Physics.ElectronGMinus2ScoreCard
  36
  37open IndisputableMonolith.Constants
  38open IndisputableMonolith.Numerics
  39
  40noncomputable section
  41
  42/-! ## Re-exported row aliases -/
  43
  44/-- P1-C05 leading electron anomaly prediction. -/
  45noncomputable def row_electron_ae_leading : ℝ :=
  46  alpha / (2 * Real.pi)
  47
  48/-- CODATA electron anomalous magnetic moment, dimensionless. -/
  49def row_electron_ae_codata : ℝ := 0.00115965218059
  50
  51private theorem alphaInv_pos : 0 < alphaInv := by
  52  linarith [alphaInv_gt]
  53
  54theorem row_electron_ae_leading_eq :
  55    row_electron_ae_leading = 1 / (2 * Real.pi * alphaInv) := by
  56  unfold row_electron_ae_leading alpha
  57  field_simp [ne_of_gt alphaInv_pos, Real.pi_ne_zero]
  58
  59private theorem ae_den_pos : 0 < 2 * Real.pi * alphaInv := by
  60  nlinarith [Real.pi_pos, alphaInv_pos]
  61
  62theorem row_electron_ae_leading_lower :
  63    (0.001161 : ℝ) < row_electron_ae_leading := by
  64  rw [row_electron_ae_leading_eq]
  65  rw [lt_div_iff₀ ae_den_pos]
  66  have hpiUB : (Real.pi : ℝ) < 3.142 := by
  67    linarith [Real.pi_lt_d6, Real.pi_pos]
  68  have h2piUB : (2 : ℝ) * Real.pi < 2 * 3.142 := by
  69    exact mul_lt_mul_of_pos_left hpiUB (by norm_num)
  70  have hden1 : (2 : ℝ) * Real.pi * alphaInv < (2 * 3.142) * alphaInv := by
  71    exact mul_lt_mul_of_pos_right h2piUB alphaInv_pos
  72  have hden2 : (2 * 3.142 : ℝ) * alphaInv < (2 * 3.142) * (137.039 : ℝ) := by
  73    exact mul_lt_mul_of_pos_left alphaInv_lt (by norm_num)
  74  have hnum : (0.001161 : ℝ) * ((2 * 3.142 : ℝ) * (137.039 : ℝ)) < 1 := by
  75    norm_num
  76  have hLpos : (0 : ℝ) < 0.001161 := by norm_num
  77  have hden : (2 : ℝ) * Real.pi * alphaInv < (2 * 3.142 : ℝ) * (137.039 : ℝ) := by
  78    linarith
  79  have hmul : (0.001161 : ℝ) * ((2 : ℝ) * Real.pi * alphaInv) <
  80      (0.001161 : ℝ) * ((2 * 3.142 : ℝ) * (137.039 : ℝ)) := by
  81    exact mul_lt_mul_of_pos_left hden hLpos
  82  linarith
  83
  84theorem row_electron_ae_leading_upper :
  85    row_electron_ae_leading < (0.001162 : ℝ) := by
  86  rw [row_electron_ae_leading_eq]
  87  rw [div_lt_iff₀ ae_den_pos]
  88  have hpiLB : (3.1415 : ℝ) < (Real.pi : ℝ) := by
  89    linarith [Real.pi_gt_d6, Real.pi_pos]
  90  have h2piLB : (2 : ℝ) * 3.1415 < 2 * Real.pi := by
  91    exact mul_lt_mul_of_pos_left hpiLB (by norm_num)
  92  have hden1 : (2 * 3.1415 : ℝ) * (137.030 : ℝ) <
  93      (2 * Real.pi) * (137.030 : ℝ) := by
  94    exact mul_lt_mul_of_pos_right h2piLB (by norm_num)
  95  have hden2 : (2 * Real.pi : ℝ) * (137.030 : ℝ) < (2 * Real.pi) * alphaInv := by
  96    exact mul_lt_mul_of_pos_left alphaInv_gt (mul_pos (by norm_num) Real.pi_pos)
  97  have hnum : 1 < (0.001162 : ℝ) * ((2 * 3.1415 : ℝ) * (137.030 : ℝ)) := by
  98    norm_num
  99  have hUpos : (0 : ℝ) < 0.001162 := by norm_num
 100  have hden : (2 * 3.1415 : ℝ) * (137.030 : ℝ) < (2 * Real.pi) * alphaInv := by
 101    linarith
 102  have hmul : (0.001162 : ℝ) * ((2 * 3.1415 : ℝ) * (137.030 : ℝ)) <
 103      (0.001162 : ℝ) * ((2 * Real.pi) * alphaInv) := by
 104    exact mul_lt_mul_of_pos_left hden hUpos
 105  linarith
 106
 107theorem row_electron_ae_leading_bracket :
 108    (0.001161 : ℝ) < row_electron_ae_leading ∧
 109      row_electron_ae_leading < (0.001162 : ℝ) :=
 110  ⟨row_electron_ae_leading_lower, row_electron_ae_leading_upper⟩
 111
 112theorem row_electron_ae_codata_pos :
 113    0 < row_electron_ae_codata := by
 114  unfold row_electron_ae_codata
 115  norm_num
 116
 117theorem row_electron_ae_schwinger_relative_residual :
 118    |row_electron_ae_leading - row_electron_ae_codata| /
 119      row_electron_ae_codata < (0.003 : ℝ) := by
 120  have hb := row_electron_ae_leading_bracket
 121  rw [div_lt_iff₀ row_electron_ae_codata_pos, abs_lt]
 122  unfold row_electron_ae_codata
 123  constructor <;> nlinarith [hb.1, hb.2]
 124
 125structure ElectronGMinus2ScoreCardCert where
 126  leading_bracket :
 127    (0.001161 : ℝ) < row_electron_ae_leading ∧
 128      row_electron_ae_leading < (0.001162 : ℝ)
 129  schwinger_residual :
 130    |row_electron_ae_leading - row_electron_ae_codata| /
 131      row_electron_ae_codata < (0.003 : ℝ)
 132
 133theorem electronGMinus2ScoreCardCert_holds :
 134    Nonempty ElectronGMinus2ScoreCardCert :=
 135  ⟨{ leading_bracket := row_electron_ae_leading_bracket
 136     schwinger_residual := row_electron_ae_schwinger_relative_residual }⟩
 137
 138end
 139
 140end IndisputableMonolith.Physics.ElectronGMinus2ScoreCard
 141