pion_electron_ratio_approx
plain-language theorem explainer
The declaration verifies that the charged pion to electron mass ratio lies within one unit of 273. Researchers modeling light meson masses on the phi-ladder in Recognition Science would cite this bound as a consistency check. The proof reduces the claim to direct substitution of the PDG mass constants followed by numerical simplification.
Claim. $|m_π⁺ / m_e - 273| < 1$, where $m_π⁺$ denotes the charged pion mass and $m_e$ the electron mass, both expressed in eV.
background
In the Pion Masses module the charged pion mass is fixed at 139.57039 MeV (converted to eV) and the electron mass at 0.51099895 × 10^6 eV; their ratio is defined directly as pionElectronRatio. The module places pions as quark-antiquark states whose masses follow phi-ladder rungs and the GMOR relation, predicting the ratio approximates 273, identified with φ^12 / 2. Upstream results supply the explicit mass constants together with the ratio definition and the identity event from ObserverForcing that anchors the J-cost minimum.
proof idea
The proof is a one-line wrapper that applies simp to unfold the ratio and mass definitions, then norm_num to confirm the absolute difference is less than 1.
why it matters
This numerical verification supports the module prediction that the pion-electron ratio approximates 273 and aligns with phi-ladder placement for mesons. It supplies a concrete check on the Recognition Science mass formula for the lightest hadrons, consistent with the eight-tick octave and D = 3 framework landmarks. No downstream theorems depend on it, leaving the result as an isolated consistency test rather than a derivation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.