row_muon_rel
plain-language theorem explainer
The row_muon_rel theorem records that the Recognition Science mass prediction for the muon on rung 13 deviates by less than four percent from the measured value 105.658 MeV. Researchers assembling lepton mass tables or verifying the phi-ladder predictions would cite this entry alongside the electron and tau rows. The proof reduces immediately to the percentage bound already established in the quark scorecard module.
Claim. $|rs_{mass,MeV}(Lepton,13) - m_μ^{exp}| / m_μ^{exp} < 0.04$ where $rs_{mass,MeV}$ is the Recognition-Science mass formula in MeV for the Lepton sector at rung 13 and $m_μ^{exp}$ is the experimental muon mass 105.6583755 MeV.
background
The ChargedLeptonMassScoreCard module treats phase-2 lepton masses via the rs_mass_MeV function on the phi-ladder for the Lepton sector at rungs 2, 13 and 19 with ZOf = 1332. The function rs_mass_MeV(s, r) computes (2)^(B_pow s) * phi^(-5) * phi^(r0 s) * phi^r / 10^6, scaling the base mass by powers of 2 and phi. The experimental muon mass is fixed at the constant 105.6583755 MeV. The upstream row_muon_pct theorem supplies the four-percent bound directly from the same rs_mass_MeV expression.
proof idea
The proof is a one-line wrapper that applies the row_muon_pct theorem from the QuarkScoreCard module.
why it matters
This declaration supplies the muon entry for the chargedLeptonMassScoreCardCert_holds theorem, which packages the three relative-error rows and two mass-ratio rows into a single certificate. It closes the muon row in the P2-LEP phase of the mass predictions, consistent with the eight-tick octave and phi-ladder structure. The same residual gap between the exponential phi formula and the computed rs_mass_MeV remains open for future refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.