pion_mass_near_140
plain-language theorem explainer
The theorem confirms that the charged pion mass, fixed at 139.57 MeV from PDG data, satisfies |m - 140| < 1. Researchers checking Recognition Science mass predictions against experiment would cite this when validating the phi-ladder rung for the lightest mesons. The proof is a one-line wrapper that unfolds the constant definition and reduces the numerical inequality via normalization.
Claim. Let $m = 139.57039$ MeV denote the charged pion mass. Then $|m - 140| < 1$.
background
The module derives pion masses from Recognition Science via quark-antiquark binding on the phi-ladder, chiral symmetry breaking, and the GMOR relation linking $m_π^2$ to quark masses and the condensate. Pions occupy a specific rung that fixes their mass relative to other hadrons, with the explicit prediction $m_{π^+} ≈ 139.6$ MeV. The upstream definition supplies the numerical value: charged pion mass in MeV (PDG 2024) given by the constant 139.57039.
proof idea
The term proof applies simp to replace the identifier with its defining constant 139.57039, then invokes norm_num to discharge the absolute-value inequality by direct arithmetic reduction.
why it matters
This result anchors the P-013 pion-mass derivation inside the Recognition framework by confirming the phi-ladder placement yields a value within 1 MeV of the conventional 140 MeV scale. It supports downstream checks of the predicted pion-to-electron ratio ≈ φ^12 / 2 and the electromagnetic mass splitting between charged and neutral pions. No open scaffolding remains; the numerical proximity is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.