pionMassDifference_MeV
plain-language theorem explainer
Pion mass difference in MeV is obtained by subtracting the neutral-pion mass from the charged-pion mass. Researchers comparing RS-derived hadron masses to PDG values cite this quantity when isolating electromagnetic corrections. The definition performs a direct numerical subtraction of the two supplied constants.
Claim. $m_{π^+} - m_{π^0}$ in MeV, where the charged-pion mass equals 139.57039 and the neutral-pion mass equals 134.9768.
background
The module places the pion on a rung of the phi-ladder after fixing quark-antiquark binding energy and applying the GMOR relation that links mass squared to the product of light-quark masses and the chiral condensate. The local setting treats the observed splitting as an electromagnetic correction once the strong-interaction baseline is set by the ladder. Upstream, Mass is an alias for the reals, and the two input masses are supplied as PDG 2024 constants.
proof idea
One-line definition that subtracts the neutral-pion mass constant from the charged-pion mass constant.
why it matters
The quantity is referenced by mass_difference_electromagnetic, which verifies an absolute splitting near 4.6 MeV, and by relativeMassDifference, which yields the 3.4 percent relative effect. It therefore supplies the numerical bridge between the RS phi-ladder prediction for the average pion mass and the measured isospin violation, consistent with the electromagnetic origin stated in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.