charged_heavier_than_neutral
plain-language theorem explainer
The theorem asserts that the charged pion mass exceeds the neutral pion mass in MeV units, matching the electromagnetic splitting seen in hadron data. Physicists comparing Recognition Science phi-ladder predictions to PDG values would cite this check for model consistency. The proof reduces to unfolding the two constant definitions and verifying the numerical inequality.
Claim. $m_{π^+} > m_{π^0}$ (in MeV), with the masses taken from the Recognition Science definitions that embed the PDG 2024 values.
background
The Pion Masses module derives π⁺, π⁻, and π⁰ masses from Recognition Science via quark-antiquark binding on the phi-ladder, chiral symmetry breaking, and the GMOR relation. Charged and neutral masses are introduced as concrete real constants: pionChargedMass_MeV := 139.57039 and pionNeutralMass_MeV := 134.9768. The module notes that the small splitting arises from electromagnetic effects while the overall scale follows the phi-ladder rung placement.
proof idea
The proof is a term-mode reduction: simp unfolds the two mass definitions, after which norm_num confirms the numerical comparison 139.57039 > 134.9768 holds.
why it matters
The result confirms the electromagnetic mass difference inside the RS pion predictions (π⁺ ≈ 139.6 MeV, π⁰ ≈ 135.0 MeV) and aligns with the module's stated mechanism. It supports consistency checks against the eight-tick octave and phi-ladder mass formulas, though no downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.