IndisputableMonolith.Masses.Basic

   1-- import IndisputableMonolith.Data.Import  -- [not in public release]
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.Assumptions
   4
   5open IndisputableMonolith.Data
   6
   7/-! Model: charged-lepton ladder surrogate. -/
   8
   9/-- Exponents for surrogate ladder differences (paper placeholder). -/
  10@[simp] def rung_exponent (name : String) : Int :=
  11  if name = "mu_e" then 11 else if name = "tau_mu" then 6 else 0
  12
  13@[simp] def mass_ladder_matches_pdg (φ : ℝ) : Prop :=
  14  ∀ m ∈ import_measurements, |m.value - φ ^ rung_exponent m.name| ≤ m.error
  15
  16/-- Pending proof: relies on `Masses.mass_ladder_assumption` (docs). -/
  17lemma mass_ladder_holds
  18    (h : Masses.mass_ladder_assumption) :
  19    mass_ladder_matches_pdg IndisputableMonolith.Constants.phi :=
  20  h
  21