relativeMassDifference
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive absolute pion masses from the phi-ladder.
- Does not include higher-order electromagnetic or quark-mass corrections.
- Does not address isospin violation beyond the mass difference.
Lean usage
simp only [relativeMassDifference, pionMassDifference_MeV, pionNeutralMass_MeV]formal statement (Lean)
150def relativeMassDifference : ℝ := pionMassDifference_MeV / pionNeutralMass_MeV * 100
proof body
Definition body.
151