ratio_mu_e_exp
plain-language theorem explainer
Defines the experimental muon-electron mass ratio as the quotient of the PDG muon mass and electron mass constants. Researchers verifying Recognition Science lepton mass predictions against data cite this ratio to test the phi^11 scaling relation. The definition performs a direct division of two imported real constants.
Claim. The experimental muon-electron mass ratio is defined as $m_μ^{exp} / m_e^{exp}$, where $m_μ^{exp} = 105.6583755$ MeV and $m_e^{exp} = 0.51099895069$ MeV are the PDG experimental masses.
background
The module compares RS mass predictions to PDG experimental values, treating the latter as imported constants rather than RS-derived quantities. The lepton mass formula uses B_pow = -22 and r0 = 62, giving m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) in MeV. Upstream definitions supply the numerical values m_e_exp := 0.51099895069 and m_mu_exp := 105.6583755.
proof idea
The definition is a one-line wrapper that divides the muon experimental mass by the electron experimental mass.
why it matters
This ratio feeds the ChargedLeptonMassScoreCardCert structure, which certifies that |φ^{11} - ratio| / ratio < 0.04. It also supports the muon_electron_ratio_error theorem and the overall MassVerificationCert. In the framework it closes the verification step for the phi fixed point applied to lepton masses, confirming the scaling within experimental bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.