pdg_muon_MeV
plain-language theorem explainer
The declaration records the Particle Data Group 2024 experimental value for the muon rest mass in MeV units as the real constant 105.66. Recognition Science modelers cite it when comparing the phi-ladder mass predictions for charged leptons against measured data. It is introduced as a direct numeric definition with no computation or lemmas.
Claim. The PDG experimental value for the muon rest mass is defined as the real number $m_μ = 105.66$ MeV.
background
The Standard Model Mass Verification module states the Recognition Science mass predictions for all Standard Model particles and compares them to PDG 2024 values. The underlying mass law is $m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z))$, with yardstick, rung r, and charge gap Z obtained from cube geometry in three dimensions and wallpaper groups. PDG comparisons are treated as experimental anchors rather than derived results.
proof idea
The definition is a direct numeric assignment of the real number 105.66 with no lemmas applied.
why it matters
This constant supplies the experimental anchor for the muon in the module's PDG comparison. It is used directly by the definitions of the muon-to-electron mass ratio and the theorem checking that ratio near 206.8. Within the Recognition Science framework it supports verification of the phi-ladder mass formula for fermions, where the muon occupies a rung position fixed by its charge and sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.