relative_difference_about_3_percent
plain-language theorem explainer
Recognition Science computes the relative pion mass splitting as approximately 3.4 percent using PDG values for the charged and neutral states. Physicists checking electromagnetic contributions to meson masses against experiment would cite this bound when validating the φ-ladder placement of pions. The proof reduces directly to unfolding the mass definitions and applying numerical normalization.
Claim. $ | ((m_{π^+} - m_{π^0}) / m_{π^0} × 100) - 3.4 | < 0.1 $, where $ m_{π^+} = 139.57039 $ MeV and $ m_{π^0} = 134.9768 $ MeV.
background
The PionMasses module derives the lightest mesons from Recognition Science via quark binding on the φ-ladder and the GMOR relation m_π² ∝ (m_u + m_d) ⟨q̄q⟩. Charged and neutral pion masses are introduced as constants: pionChargedMass_MeV := 139.57039 and pionNeutralMass_MeV := 134.9768. The mass difference is defined as pionMassDifference_MeV := pionChargedMass_MeV - pionNeutralMass_MeV, and the relative quantity is relativeMassDifference := pionMassDifference_MeV / pionNeutralMass_MeV * 100.
proof idea
The term proof is a one-line wrapper. It applies simp only to unfold relativeMassDifference together with the three mass constants, then invokes norm_num to discharge the resulting numerical inequality |3.403 - 3.4| < 0.1.
why it matters
The declaration supplies the numerical anchor for the electromagnetic splitting inside the GMOR section of the PionMasses module. It confirms consistency with the φ-ladder rung assigned to pions and the predicted m_π / m_e ratio near φ^12 / 2. No downstream theorems are recorded, leaving the result as a self-contained verification step rather than a lemma for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.