mass_difference_electromagnetic
plain-language theorem explainer
The theorem states that the absolute difference between the computed pion mass splitting and 4.6 MeV is less than 0.1. Physicists using Recognition Science for hadron spectra would cite it to verify that the electromagnetic contribution to charged-neutral pion splitting aligns with PDG data within the stated tolerance. The proof is a one-line wrapper that unfolds the difference definition via simp and evaluates the numerical bound with norm_num.
Claim. $| (m_{π^+} - m_{π^0}) - 4.6 | < 0.1$ (masses in MeV), where the difference is obtained by subtracting the neutral-pion mass from the charged-pion mass.
background
In the Pion Masses module the pions are treated as quark-antiquark states whose masses follow φ-ladder placement, with the charged-neutral splitting attributed to electromagnetic effects after the strong-interaction contribution is fixed by the Recognition Composition Law and the J-cost function. The upstream definitions supply the numerical inputs: pionChargedMass_MeV := 139.57039, pionNeutralMass_MeV := 134.9768, and pionMassDifference_MeV := pionChargedMass_MeV - pionNeutralMass_MeV, all typed as Mass (an abbreviation for ℝ). The module doc-comment frames this as part of the GMOR relation and explicit chiral-symmetry breaking within the RS-native units where c = 1 and ħ = φ^{-5}.
proof idea
The term proof applies simp only to the three sibling definitions, which substitutes the concrete real numbers for the charged and neutral masses, then invokes norm_num to reduce the absolute-value inequality to a decidable numerical comparison that succeeds automatically.
why it matters
The declaration closes the numerical check for the electromagnetic mass difference listed in the module predictions (π⁺ - π⁰ ≈ 4.6 MeV). It supports the broader P-013 claim that the pion occupies a definite rung on the φ-ladder and that the observed splitting is consistent with the RS eight-tick octave structure. No downstream theorems currently depend on it, leaving open the question of whether the same difference can be derived from the J-uniqueness axiom without importing PDG values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.