ratio_mu_e_exp
plain-language theorem explainer
Defines the experimental muon-to-electron mass ratio as the quotient of the PDG 2024 MeV values. Anyone comparing RS lepton ladder predictions to data cites this constant. The body is a one-line division of the two imported experimental masses; no proof content.
Claim. Let $m_\mu^{\mathrm{exp}} = 105.6583755\,\mathrm{MeV}$ and $m_e^{\mathrm{exp}} = 0.51099895069\,\mathrm{MeV}$ be the PDG 2024 central values. The experimental ratio is $m_\mu^{\mathrm{exp}} / m_e^{\mathrm{exp}} \in \mathbb{R}$.
background
The MassComparison module is quarantined from the certified RS surface: it imports PDG 2024 numbers rather than deriving them, and mass predictions sit on the $\varphi$-ladder with sector yardsticks. Experimental electron and muon masses are fixed as bare real constants ($0.51099895069$ MeV and $105.6583755$ MeV).
In RS, lepton masses take the form yardstick(sector) $\times \varphi^{r_0 + r_{\mathrm{species}}}$, with $E_{\mathrm{coh}} = \varphi^{-5}$. The electron sits at rung 2; the muon is compared via a pure power of $\varphi$ (classically $\varphi^{11}$) against this experimental ratio. Upstream, the same ratio is re-exported in Masses.Verification for certificate packing.
proof idea
Pure definition: unfold to the quotient of the two experimental mass constants already present in the module. No tactics, no lemmas, no noncomputable choice beyond the ambient real division.
why it matters
Feeds the quantitative muon checks that close the lepton sector of the mass verification certificate. Downstream, muon_ratio_undershoot proves $\varphi^{11}$ lies strictly below this ratio; muon_electron_ratio_error bounds the relative error by $4%$; ratio_mu_e_exp_bounds and ratio_mu_e_exp_value pin the numerical window near $206.77$. Those facts enter MassVerificationCert (muon percent and range fields) and the raw prediction discrepancy score in this module. The comparison is the empirical half of the $\varphi$-ladder mass formula against PDG 2024, not a derivation of the rung itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.