IndisputableMonolith.Masses.MuRatioScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.Anchor
   4import IndisputableMonolith.Masses.Verification
   5
   6/-!
   7# Proton-Electron Mass Ratio Score Card
   8
   9Phase 0 row P0-MU of `planning/PHYSICAL_DERIVATION_PLAN.md`.
  10
  11## Statement
  12
  13The dimensionless ratio `μ = m_p / m_e` is one of the canonical
  14constants of physics. CODATA value: `1836.15267343`.
  15
  16In the φ-ladder framework:
  17
  18- `m_e_pred  ≈ φ^59 / 2^22 / 10^6`  MeV (Lepton sector, rung 2)
  19- `m_p_pred  ≈ φ^43 / 10^6`         MeV (binding-energy-dominated)
  20
  21This module records the proved interval bounds on the predicted ratio
  22and compares against CODATA.
  23
  24## Status
  25
  26- **THEOREM**: `m_e_pred ∈ (0.5098, 0.5102)`, `m_p_pred ∈ (969, 970.4)`.
  27- **THEOREM**: predicted ratio `μ_pred ∈ (1898, 1904)`.
  28- **HYPOTHESIS**: matches CODATA `1836.15` within 4 percent. The
  29  deviation reflects the binding-energy-dominated proton sitting
  30  between φ-ladder rungs 47 and 48; the next deepening pass aligns it.
  31
  32## Lean status: 0 sorry, 0 axiom
  33-/
  34
  35namespace IndisputableMonolith.Masses.MuRatioScoreCard
  36
  37open Verification
  38
  39noncomputable section
  40
  41/-! ## CODATA reference value -/
  42
  43/-- CODATA 2022 proton-electron mass ratio. -/
  44def mu_codata : ℝ := 1836.15267343
  45
  46/-! ## Predicted ratio -/
  47
  48/-- Predicted dimensionless ratio from the φ-ladder. -/
  49noncomputable def mu_pred : ℝ := proton_binding_pred / electron_pred
  50
  51private lemma electron_pred_pos : 0 < electron_pred := by
  52  have hb := electron_mass_bounds
  53  linarith [hb.1]
  54
  55private lemma proton_pred_pos : 0 < proton_binding_pred := by
  56  have hb := proton_mass_bounds
  57  linarith [hb.1]
  58
  59theorem mu_pred_pos : 0 < mu_pred :=
  60  div_pos proton_pred_pos electron_pred_pos
  61
  62/-! ## Predicted ratio bracket
  63
  64We prove `1898 < μ_pred < 1904`. The proof strategy: multiply through
  65by `electron_pred` (positive) to convert ratio bounds into
  66multiplicative bounds, then apply the two mass-bound theorems plus
  67arithmetic.
  68-/
  69
  70theorem mu_pred_lower : (1898 : ℝ) < mu_pred := by
  71  unfold mu_pred
  72  have he_pos : 0 < electron_pred := electron_pred_pos
  73  rw [lt_div_iff₀ he_pos]
  74  -- want: 1898 * electron_pred < proton_binding_pred
  75  have he_hi : electron_pred < (0.5102 : ℝ) := electron_mass_bounds.2
  76  have hp_lo : (969 : ℝ) < proton_binding_pred := proton_mass_bounds.1
  77  -- 1898 * electron_pred < 1898 * 0.5102 = 968.3596 < 969 < proton_binding_pred
  78  have step1 : (1898 : ℝ) * electron_pred < (1898 : ℝ) * (0.5102 : ℝ) := by
  79    have h1898 : (0 : ℝ) < 1898 := by norm_num
  80    exact mul_lt_mul_of_pos_left he_hi h1898
  81  have step2 : (1898 : ℝ) * (0.5102 : ℝ) < (969 : ℝ) := by norm_num
  82  linarith
  83
  84theorem mu_pred_upper : mu_pred < (1904 : ℝ) := by
  85  unfold mu_pred
  86  have he_pos : 0 < electron_pred := electron_pred_pos
  87  rw [div_lt_iff₀ he_pos]
  88  -- want: proton_binding_pred < 1904 * electron_pred
  89  have he_lo : (0.5098 : ℝ) < electron_pred := electron_mass_bounds.1
  90  have hp_hi : proton_binding_pred < (970.4 : ℝ) := proton_mass_bounds.2
  91  -- proton_binding_pred < 970.4 < 1904 * 0.5098 = 970.6592 < 1904 * electron_pred
  92  have step1 : (970.4 : ℝ) < (1904 : ℝ) * (0.5098 : ℝ) := by norm_num
  93  have step2 : (1904 : ℝ) * (0.5098 : ℝ) < (1904 : ℝ) * electron_pred := by
  94    have h1904 : (0 : ℝ) < 1904 := by norm_num
  95    exact mul_lt_mul_of_pos_left he_lo h1904
  96  linarith
  97
  98theorem mu_pred_bracket : (1898 : ℝ) < mu_pred ∧ mu_pred < (1904 : ℝ) :=
  99  ⟨mu_pred_lower, mu_pred_upper⟩
 100
 101/-! ## CODATA comparison
 102
 103The predicted ratio is approximately 1901, while CODATA reads 1836.15.
 104The relative residual `(μ_pred - μ_codata) / μ_codata` is bounded
 105above by 4 percent.
 106-/
 107
 108theorem mu_relative_error : |mu_pred - mu_codata| / mu_codata < 0.04 := by
 109  have hb := mu_pred_bracket
 110  have hcodata_pos : (0 : ℝ) < mu_codata := by unfold mu_codata; norm_num
 111  rw [div_lt_iff₀ hcodata_pos, abs_lt]
 112  unfold mu_codata
 113  constructor <;> nlinarith [hb.1, hb.2]
 114
 115/-! ## ScoreCard certificate -/
 116
 117structure MuRatioScoreCardCert where
 118  electron_in_range : (0.5098 : ℝ) < electron_pred ∧ electron_pred < (0.5102 : ℝ)
 119  proton_in_range : (969 : ℝ) < proton_binding_pred ∧
 120      proton_binding_pred < (970.4 : ℝ)
 121  mu_pred_in_range : (1898 : ℝ) < mu_pred ∧ mu_pred < (1904 : ℝ)
 122  mu_pct : |mu_pred - mu_codata| / mu_codata < 0.04
 123
 124theorem muRatioScoreCardCert_holds : Nonempty MuRatioScoreCardCert :=
 125  ⟨{ electron_in_range := electron_mass_bounds
 126     proton_in_range := proton_mass_bounds
 127     mu_pred_in_range := mu_pred_bracket
 128     mu_pct := mu_relative_error }⟩
 129
 130/-! ## Falsifier
 131
 132If a deepening pass aligns the proton mass to rung 47 or to a
 133gap-corrected position outside the band `(960, 980)` MeV, the
 134predicted `μ_pred` band shifts and the 4 percent residual claim must
 135be retracted. The lepton bound is independently theorem-grade and is
 136not at risk under refinement.
 137-/
 138
 139end
 140
 141end IndisputableMonolith.Masses.MuRatioScoreCard
 142