def
definition
phi_12
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.PionMasses on GitHub at line 136.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
133 constructor <;> linarith
134
135/-- φ^12 ≈ 322, close to 273 × (E_coh conversion). -/
136def phi_12 : ℝ := phi ^ 12
137
138/-! ## Mass Difference -/
139
140/-- π⁺ - π⁰ mass difference in MeV. -/
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. -/