row_muon_electron_ratio
plain-language theorem explainer
The muon-electron PDG mass ratio lies within 4 percent of phi to the eleventh power. Researchers assembling the charged-lepton mass scorecard in Recognition Science cite this result to confirm the relative-error row for the P2-LEP phase. The declaration is a one-line wrapper that directly invokes the percentage-error theorem already proved in the quark scorecard module.
Claim. $|phi^{11} - (m_μ / m_e)_{exp}| / (m_μ / m_e)_{exp} < 0.04$, where phi is the self-similar fixed point of Recognition Science and the masses are the experimental PDG values.
background
The module verifies charged-lepton masses on the phi-ladder: rs_mass_MeV evaluated at rungs 2, 13 and 19 with ZOf = 1332, compared against PDG references m_e_exp, m_mu_exp and m_tau_exp. The upstream theorem row_muon_electron_ratio_pct states that the muon-electron PDG mass ratio matches phi^11 within 4 percent. Its supporting definition ratio_mu_e_exp is simply m_mu_exp / m_e_exp.
proof idea
One-line wrapper that applies row_muon_electron_ratio_pct from QuarkScoreCard, which itself reduces to Verification.muon_electron_ratio_error.
why it matters
The result supplies the muon-electron entry inside ChargedLeptonMassScoreCardCert and is witnessed by chargedLeptonMassScoreCardCert_holds. It advances the partial theorem on relative errors for the lepton mass rows, consistent with the mass formula yardstick * phi^(rung-8+gap(Z)) and the T6 forcing of phi as self-similar fixed point. It leaves open the gap/anchor residual that would be required to equate rs_mass_MeV exactly with the absolute PDG masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.