  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.