IndisputableMonolith.Constants.HartreeRydbergScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants.Alpha
   3import IndisputableMonolith.Numerics.Interval.AlphaBounds
   4
   5/-!
   6# Hartree, Rydberg, and Bohr Dimensionless Score Card
   7
   8Phase 1 rows **P1-C04** (Hartree energy) and **P1-C02** (Rydberg
   9constant / hydrogen ground binding scale), plus **P1-C03** (Bohr radius)
  10in
  11`planning/PHYSICAL_DERIVATION_PLAN.md`.
  12
  13## Statement
  14
  15The theorem-grade, unit-free content is:
  16
  17* `E_h / (m_e c^2) = α^2`
  18* `E_R / (m_e c^2) = α^2 / 2`
  19* `a_0 / λbar_C = 1/α`
  20
  21using the certified RS inverse fine-structure constant `alphaInv`.
  22
  23## Measurement target
  24
  25CODATA / NIST Hartree, Rydberg, and Bohr-radius constants in SI units.
  26This module does not claim a Joule or meter value, because that requires
  27the electron-mass, `h`, `c`, and SI display bridge. It records the
  28dimensionless ratios and their tight interval bounds.
  29
  30Falsifier: CODATA `α^-1` outside `(137.030, 137.039)` or an SI bridge that
  31does not map the dimensionless `α²` / `α²/2` ratios to Hartree/Rydberg
  32measurements.
  33
  34## Lean status: 0 sorry, 0 axiom
  35-/
  36
  37namespace IndisputableMonolith.Constants.HartreeRydbergScoreCard
  38
  39open IndisputableMonolith.Constants
  40open IndisputableMonolith.Numerics
  41
  42noncomputable section
  43
  44/-! ## Re-exported row aliases -/
  45
  46/-- P1-C04 dimensionless Hartree/rest-energy ratio. -/
  47noncomputable def row_hartree_over_rest : ℝ := alpha ^ 2
  48
  49/-- P1-C02 dimensionless Rydberg/rest-energy ratio. -/
  50noncomputable def row_rydberg_over_rest : ℝ := alpha ^ 2 / 2
  51
  52/-- P1-C03 dimensionless Bohr/reduced-Compton radius ratio. -/
  53noncomputable def row_bohr_over_reduced_compton : ℝ := alphaInv
  54
  55private theorem alphaInv_pos : 0 < alphaInv := by
  56  linarith [alphaInv_gt]
  57
  58theorem row_hartree_over_rest_eq : row_hartree_over_rest = 1 / alphaInv ^ 2 := by
  59  unfold row_hartree_over_rest alpha
  60  field_simp [ne_of_gt alphaInv_pos]
  61
  62theorem row_rydberg_over_rest_eq :
  63    row_rydberg_over_rest = 1 / (2 * alphaInv ^ 2) := by
  64  unfold row_rydberg_over_rest alpha
  65  field_simp [ne_of_gt alphaInv_pos]
  66
  67/-! ## Certified interval bounds -/
  68
  69theorem row_hartree_over_rest_lower :
  70    (5.32e-5 : ℝ) < row_hartree_over_rest := by
  71  rw [row_hartree_over_rest_eq]
  72  have hpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
  73  rw [lt_div_iff₀ hpos]
  74  have hsq : alphaInv ^ 2 < (137.039 : ℝ) ^ 2 := by
  75    nlinarith [alphaInv_lt, alphaInv_gt]
  76  have hnum : (5.32e-5 : ℝ) * (137.039 : ℝ) ^ 2 < 1 := by norm_num
  77  nlinarith
  78
  79theorem row_hartree_over_rest_upper :
  80    row_hartree_over_rest < (5.33e-5 : ℝ) := by
  81  rw [row_hartree_over_rest_eq]
  82  have hpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
  83  rw [div_lt_iff₀ hpos]
  84  have hsq : (137.030 : ℝ) ^ 2 < alphaInv ^ 2 := by
  85    nlinarith [alphaInv_gt, alphaInv_lt]
  86  have hnum : 1 < (5.33e-5 : ℝ) * (137.030 : ℝ) ^ 2 := by norm_num
  87  nlinarith
  88
  89theorem row_hartree_over_rest_bracket :
  90    (5.32e-5 : ℝ) < row_hartree_over_rest ∧
  91      row_hartree_over_rest < (5.33e-5 : ℝ) :=
  92  ⟨row_hartree_over_rest_lower, row_hartree_over_rest_upper⟩
  93
  94theorem row_rydberg_over_rest_lower :
  95    (2.66e-5 : ℝ) < row_rydberg_over_rest := by
  96  rw [row_rydberg_over_rest_eq]
  97  have hsqpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
  98  have hpos : 0 < 2 * alphaInv ^ 2 := by nlinarith
  99  rw [lt_div_iff₀ hpos]
 100  have hsq : alphaInv ^ 2 < (137.039 : ℝ) ^ 2 := by
 101    nlinarith [alphaInv_lt, alphaInv_gt]
 102  have hnum : (2.66e-5 : ℝ) * (2 * (137.039 : ℝ) ^ 2) < 1 := by norm_num
 103  nlinarith
 104
 105theorem row_rydberg_over_rest_upper :
 106    row_rydberg_over_rest < (2.665e-5 : ℝ) := by
 107  rw [row_rydberg_over_rest_eq]
 108  have hsqpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
 109  have hpos : 0 < 2 * alphaInv ^ 2 := by nlinarith
 110  rw [div_lt_iff₀ hpos]
 111  have hsq : (137.030 : ℝ) ^ 2 < alphaInv ^ 2 := by
 112    nlinarith [alphaInv_gt, alphaInv_lt]
 113  have hnum : 1 < (2.665e-5 : ℝ) * (2 * (137.030 : ℝ) ^ 2) := by norm_num
 114  nlinarith
 115
 116theorem row_rydberg_over_rest_bracket :
 117    (2.66e-5 : ℝ) < row_rydberg_over_rest ∧
 118      row_rydberg_over_rest < (2.665e-5 : ℝ) :=
 119  ⟨row_rydberg_over_rest_lower, row_rydberg_over_rest_upper⟩
 120
 121theorem row_bohr_over_reduced_compton_eq :
 122    row_bohr_over_reduced_compton = alphaInv := rfl
 123
 124theorem row_bohr_over_reduced_compton_bracket :
 125    (137.030 : ℝ) < row_bohr_over_reduced_compton ∧
 126      row_bohr_over_reduced_compton < (137.039 : ℝ) :=
 127  ⟨alphaInv_gt, alphaInv_lt⟩
 128
 129structure HartreeRydbergScoreCardCert where
 130  hartree_closed : row_hartree_over_rest = 1 / alphaInv ^ 2
 131  rydberg_closed : row_rydberg_over_rest = 1 / (2 * alphaInv ^ 2)
 132  bohr_closed : row_bohr_over_reduced_compton = alphaInv
 133  hartree_bracket :
 134    (5.32e-5 : ℝ) < row_hartree_over_rest ∧
 135      row_hartree_over_rest < (5.33e-5 : ℝ)
 136  rydberg_bracket :
 137    (2.66e-5 : ℝ) < row_rydberg_over_rest ∧
 138      row_rydberg_over_rest < (2.665e-5 : ℝ)
 139  bohr_bracket :
 140    (137.030 : ℝ) < row_bohr_over_reduced_compton ∧
 141      row_bohr_over_reduced_compton < (137.039 : ℝ)
 142
 143theorem hartreeRydbergScoreCardCert_holds :
 144    Nonempty HartreeRydbergScoreCardCert :=
 145  ⟨{ hartree_closed := row_hartree_over_rest_eq
 146     rydberg_closed := row_rydberg_over_rest_eq
 147     bohr_closed := row_bohr_over_reduced_compton_eq
 148     hartree_bracket := row_hartree_over_rest_bracket
 149     rydberg_bracket := row_rydberg_over_rest_bracket
 150     bohr_bracket := row_bohr_over_reduced_compton_bracket }⟩
 151
 152end
 153
 154end IndisputableMonolith.Constants.HartreeRydbergScoreCard
 155