relativeMassDifference
plain-language theorem explainer
The definition computes the percentage mass splitting between charged and neutral pions from their MeV values. Hadron spectroscopists or Recognition Science mass-ladder users cite it to quantify the electromagnetic contribution to the pion splitting. It is a direct arithmetic definition that divides the precomputed difference by the neutral mass and multiplies by 100.
Claim. The relative mass difference is defined by $r = 100(m_+-m_0)/m_0$ where $m_+$ and $m_0$ are the charged and neutral pion masses in MeV.
background
In the Pion Masses module the pions are treated as quark-antiquark states whose masses follow the phi-ladder. The upstream definitions supply the inputs: pionMassDifference_MeV is the charged-minus-neutral splitting (electromagnetic, ~4.6 MeV) and pionNeutralMass_MeV is the PDG value 134.9768 MeV. The module derives both absolute masses from the Recognition Science phi-ladder placement and the GMOR relation before forming this ratio.
proof idea
One-line definition that applies the arithmetic quotient of the upstream mass difference and neutral mass, then scales by 100.
why it matters
It supplies the numerical input to the downstream theorem relative_difference_about_3_percent that confirms the splitting is 3.4 percent within 0.1 percent. The result closes the electromagnetic correction step in the RS pion-mass derivation (P-013) and links the phi-ladder rung assignment to the observed charged-neutral splitting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.