pdg_mu_e_ratio_approx
plain-language theorem explainer
The declaration verifies that the PDG experimental ratio of muon to electron masses lies within one unit of 206.8. Researchers comparing Recognition Science mass predictions against particle data group values would reference this bound. The proof proceeds by unfolding the ratio definition into the supplied PDG constants and invoking numerical normalization.
Claim. Let $r = m_μ / m_e$ denote the PDG experimental ratio of muon mass to electron mass in MeV. Then $|r - 206.8| < 1$.
background
The module Standard Model Mass Verification formally states RS mass predictions for all Standard Model particles and documents their comparison with PDG 2024 experimental values. The underlying mass law is $m$(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z)), where yardstick, r, and Z are derived from cube geometry (D=3), wallpaper groups, and charge structure with zero free parameters. This theorem supplies a numerical check on the muon-electron ratio using the definitions pdg_muon_MeV := 105.66 and pdg_electron_MeV := 0.511, whose ratio is pdg_mu_e_ratio.
proof idea
The proof is a one-line wrapper that applies simplification to unfold pdg_mu_e_ratio into the quotient of the muon and electron PDG constants, followed by numerical normalization to establish the bound.
why it matters
This numerical verification supports the PDG comparison section of the mass law documentation in SMVerification. It anchors the Recognition Science framework's claim that the phi-ladder mass formula reproduces experimental values without free parameters, consistent with the eight-tick octave and D=3 spatial dimensions. No downstream theorems depend on it directly, leaving the full interval-arithmetic verification of theoretical predictions as an open step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.