mass_muon_PDG_sigma
plain-language theorem explainer
Numeric constant equal to the PDG 1σ uncertainty on the muon rest mass, 2.3×10^{-6} MeV. Used when comparing Recognition Science lepton-mass predictions against experimental bands. Pure data binding: a real literal with no proof obligation.
Claim. The Particle Data Group one-standard-deviation uncertainty on the muon rest mass is fixed as the real number $\sigma_{m_\mu}^{\mathrm{PDG}} = 0.0000023\,\mathrm{MeV}$.
background
The module Verification.PDGComparison is quarantined from the certified RS surface: it imports external experimental numbers (PDG 2024, CODATA 2022) solely for informational comparison, not as part of the forcing chain.
Sibling constants bind the central values and uncertainties for the three charged leptons and for $\alpha^{-1}$. The muon entry pairs a central mass mass_muon_PDG with this sigma. Units are MeV, matching the usual PDG tabulation $m_\mu = 105.6583755(23),\mathrm{MeV}$.
RS lepton masses themselves live on the $\varphi$-ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$); this constant is only the experimental error bar against which those predictions are scored.
proof idea
Definitional binding of a real literal. No tactics, no lemmas, no reduction: the right-hand side is the decimal $0.0000023$ inhabiting $\mathbb{R}$.
why it matters
Supplies the experimental width needed to state whether an RS muon-mass prediction lies inside the PDG band. The module's headline comparison is the $\alpha^{-1}$ interval (RS $137.030$–$137.039$ containing CODATA), but the same pattern is applied to lepton masses. Downstream use is informational only; the constant does not feed T0–T8, RCL, or the certified mass-ladder theorems. It keeps the quarantine boundary explicit: experiment enters as named data, never as a hypothesis inside a proved claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.