row_muon_pct
plain-language theorem explainer
The theorem shows that the Recognition Science muon mass prediction differs from the experimental PDG value by less than four percent. Mass spectrum modelers comparing phi-ladder formulas to data would cite this bound when validating lepton entries. The proof is a one-line term that invokes the muon_relative_error fact from the Verification module.
Claim. $ | rs_mass_MeV(Lepton, 13) - m_{μ,exp} | / m_{μ,exp} < 0.04 $
background
The QuarkScoreCard module consolidates theorem-grade facts about fermion masses in Recognition Science, recording ZOf assignments (276 for up-type quarks, 24 for down-type, 1332 for charged leptons) and noting that equal-Z fermions have anchor mass ratios that are pure φ-powers of rung differences. The rs_mass_MeV function from Verification computes base masses on the phi-ladder in MeV using the J-cost from PhiForcingDerived and ledger factorization from DAlembert, without the gap(ZOf f) correction from RSBridge.Anchor.massAtAnchor. This entry addresses the muon (Lepton index 13) and its comparison to m_mu_exp. Upstream, SpectralEmergence forces three generations and 24 chiral fermions while PhysicsComplexityStructure establishes convexity of J-cost minimization at x=1.
proof idea
The proof is a one-line wrapper that applies the muon_relative_error lemma from the Verification module, which directly establishes the same relative error bound.
why it matters
This supplies the muon component for quarkScoreCardCert_holds, which certifies the full scorecard with ZOf values and ratio equalities, and is reused in ChargedLeptonMassScoreCard.row_muon_rel. It fills the Phase 0 lepton verification row in the physical derivation plan. In the framework it confirms numerical consistency of the phi-ladder mass formula (T5 J-uniqueness, T6 phi fixed point) for the muon, though the bridge equivalence with gap correction remains open per the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.