m_mu_exp
The declaration supplies the PDG experimental muon mass in MeV as a fixed real constant. Verification routines in the lepton scorecard cite it to bound the relative error between the phi-ladder prediction and measured data. It enters as a direct numerical assignment with no internal derivation or proof steps.
claim$m_μ^{exp} := 105.6583755$ (MeV)
background
The module treats experimental masses as imported constants quarantined from the certified RS surface. For the lepton sector the integer-rung formula reads $m(Lepton,r) = φ^{57+r}/(2^{22}×10^6)$ MeV with $B_{pow}=-22$ and $r_0=62$. PDG 2024 supplies the reference value used to test the gap-corrected massAtAnchor expression against data.
proof idea
Direct definition that binds the literal 105.6583755 to the identifier m_mu_exp.
why it matters in Recognition Science
It supplies the experimental anchor for the muon row inside ChargedLeptonMassScoreCardCert and MassVerificationCert, where the relative error |rs_mass_MeV .Lepton 13 - m_mu_exp|/m_mu_exp is required to stay below 0.04. The same constant appears in QuarkScoreCardCert and the muon_relative_error theorem, closing one verification link in the T5-T8 forcing chain. It leaves open whether future derivations from the J-cost functional equation can replace the imported PDG datum.
scope and limits
- Does not derive the numerical value from the Recognition Science functional equation.
- Does not include PDG uncertainty intervals.
- Does not certify agreement for any particle outside the listed scorecard rows.
- Does not extend the comparison beyond the stated 4 percent tolerance.
formal statement (Lean)
37def m_mu_exp : ℝ := 105.6583755