row_muon_electron_ratio_pct
plain-language theorem explainer
The experimental muon-electron mass ratio satisfies |phi^11 minus the ratio| divided by the ratio is less than 0.04. Particle physicists checking phi-ladder predictions for lepton masses would cite this bound as a verified data match. The proof is a direct one-line application of the pre-established error theorem in the Verification module.
Claim. $|phi^{11} - (m_μ / m_e)_{exp}| / (m_μ / m_e)_{exp} < 0.04$, where phi is the Recognition Science self-similar fixed point and the masses are PDG experimental values.
background
The Quark Score Card module consolidates existing theorem-grade mass predictions for quarks and leptons, recording which facts are proved and which remain open without adding new physics. ratio_mu_e_exp is the definition m_mu_exp / m_e_exp. The upstream Constants structure supplies the Recognition Science parameters including phi, while muon_electron_ratio_error supplies the explicit numerical bound derived from phi^11 inequalities and experimental ratio bounds.
proof idea
One-line wrapper that applies the muon_electron_ratio_error theorem from the Verification module.
why it matters
This bound populates the row in ChargedLeptonMassScoreCard for the muon-electron ratio, confirming phi^11 scaling as part of the mass ladder. It aligns with the T6 phi fixed point and the eight-tick octave from the forcing chain. It touches the open question of absolute mass matches once the gap(ZOf) correction from RSBridge.Anchor is incorporated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.