m_e_exp
plain-language theorem explainer
The declaration supplies the PDG experimental electron mass in MeV as a real constant for use in verification. Recognition Science mass-prediction work cites it to bound relative errors between the phi-ladder formula and data. It enters by direct numerical assignment with no further reduction.
Claim. Let $m_e^exp$ denote the experimental electron rest mass in MeV, with value $m_e^exp = 0.51099895069$.
background
In the Masses.Verification module experimental masses remain imported constants, quarantined from certified RS derivations. The local formula for lepton masses is $m(Lepton,r) = φ^{57+r}/(2^{22}×10^6)$ MeV with B_pow = -22 and r0 = 62. The rs_mass_MeV function (defined upstream in Anchor) supplies the integer-rung prediction that is compared against this constant.
proof idea
The declaration is a direct definition that assigns the literal 0.51099895069 to m_e_exp. No lemmas or tactics are applied.
why it matters
It anchors the electron row of ChargedLeptonMassScoreCardCert and MassVerificationCert, both of which require |rs_mass_MeV .Lepton 2 - m_e_exp| / m_e_exp < 0.003. The definition therefore closes the experimental side of the lepton scorecard comparison inside the Recognition Science framework while remaining outside the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.