mass_difference_electromagnetic

formal source

 141def pionMassDifference_MeV : ℝ := pionChargedMass_MeV - pionNeutralMass_MeV
 142
 143/-- Mass difference is about 4.6 MeV (electromagnetic). -/
 144theorem mass_difference_electromagnetic :
 145    abs (pionMassDifference_MeV - 4.6) < 0.1 := by
 146  simp only [pionMassDifference_MeV, pionChargedMass_MeV, pionNeutralMass_MeV]
 147  norm_num
 148
 149/-- Mass difference / (neutral mass) ≈ 3.4%. -/
 150def relativeMassDifference : ℝ := pionMassDifference_MeV / pionNeutralMass_MeV * 100
 151
 152theorem relative_difference_about_3_percent :
 153    abs (relativeMassDifference - 3.4) < 0.1 := by
 154  -- ((139.57039 - 134.9768) / 134.9768) * 100 = (4.59359 / 134.9768) * 100 ≈ 3.403
 155  -- |3.403 - 3.4| = 0.003 < 0.1
 156  simp only [relativeMassDifference, pionMassDifference_MeV, pionChargedMass_MeV, pionNeutralMass_MeV]
 157  norm_num
 158
 159/-! ## GMOR Relation -/
 160
 161/-- GMOR relation: m_π² ∝ (m_u + m_d).
 162    Light quark masses (MeV): m_u ≈ 2.2, m_d ≈ 4.7.
 163    Average: (m_u + m_d)/2 ≈ 3.45 MeV. -/
 164def lightQuarkMass_MeV : ℝ := (2.2 + 4.7) / 2
 165
 166/-- Pion decay constant f_π ≈ 92.2 MeV. -/
 167def pionDecayConstant_MeV : ℝ := 92.2
 168
 169/-- Quark condensate <q̄q>^(1/3) ≈ -250 MeV. -/
 170def quarkCondensate_MeV : ℝ := 250
 171
 172/-- GMOR check: m_π² ≈ 2 × m_q × ⟨q̄q⟩ / f_π². -/
 173def gmorPrediction : ℝ :=
 174  2 * lightQuarkMass_MeV * (quarkCondensate_MeV^3) / (pionDecayConstant_MeV^2)