`row_electron_pct`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.QuarkScoreCard
domain: Masses
line: 125 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.QuarkScoreCard on GitHub at line 125.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 122-/
 123
 124/-- Electron mass within 0.3 percent of PDG. -/
 125theorem row_electron_pct :
 126    |Verification.rs_mass_MeV .Lepton 2 - Verification.m_e_exp| /
 127        Verification.m_e_exp < 0.003 :=
 128  Verification.electron_relative_error
 129
 130/-- Muon mass within 4 percent of PDG. -/
 131theorem row_muon_pct :
 132    |Verification.rs_mass_MeV .Lepton 13 - Verification.m_mu_exp| /
 133        Verification.m_mu_exp < 0.04 :=
 134  Verification.muon_relative_error
 135
 136/-- Tau mass within 3 percent of PDG. -/
 137theorem row_tau_pct :
 138    |Verification.rs_mass_MeV .Lepton 19 - Verification.m_tau_exp| /
 139        Verification.m_tau_exp < 0.03 :=
 140  Verification.tau_relative_error
 141
 142/-- Muon-electron PDG mass ratio matches `phi^11` within 4 percent. -/
 143theorem row_muon_electron_ratio_pct :
 144    |Constants.phi ^ (11 : ℕ) - Verification.ratio_mu_e_exp| /
 145        Verification.ratio_mu_e_exp < 0.04 :=
 146  Verification.muon_electron_ratio_error
 147
 148/-- Tau-electron PDG mass ratio matches `phi^17` within 3 percent. -/
 149theorem row_tau_electron_ratio_pct :
 150    |Constants.phi ^ (17 : ℕ) - Verification.ratio_tau_e_exp| /
 151        Verification.ratio_tau_e_exp < 0.03 :=
 152  Verification.tau_electron_ratio_error
 153
 154/-! ## The named open residual
 155

papers checked against this theorem

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