Physics Pion Masses

The pion mass ladder

Pions are the lightest mesons, particles made of one quark and one antiquark bound by the strong force. There are three of them: two charged pions, π⁺ and π⁻, and a neutral pion, π⁰. The charged pions have a measured mass of 139.57039 MeV, and the neutral pion is lighter at 134.9768 MeV, a difference of about 4.6 MeV that arises from electromagnetic effects. The charged pion is about 273 times heavier than the electron, a ratio close to 273.13.

The Gell-Mann–Oakes–Renner (GMOR) relation connects the pion mass to the quark masses and the chiral condensate: m_π² ∝ (m_u + m_d) × ⟨q̄q⟩. In the chiral limit, where quark masses vanish, pions would be massless Goldstone bosons; their small nonzero masses come from explicit chiral symmetry breaking. The framework's module defines a GMOR prediction using a light quark mass of 3.45 MeV, a quark condensate of 250 MeV, and a pion decay constant of 92.2 MeV, yielding a value around 12682, which the module proves lies between 100 and 100000.

In Recognition Science, the pion occupies a specific rung on a φ-ladder, where φ is the golden ratio. The module defines the pion rung as 12 and predicts the charged pion mass as E_coh × φ¹² / 2, where E_coh is a coherence energy. The theorem phi_12_div_2 proves that φ¹² / 2 is within 1 of 161, and the module shows the charged pion mass is within 1 MeV of 140 MeV. The ratio m_π/m_e ≈ 273 ≈ φ¹² / 2 is stated in the docstring as a prediction, not a proved equality.

The module also establishes structural facts about the pion: it has spin 0, isospin 1, parity -1, and forms a multiplet of 3, matching the observed triplet. A theorem proves that 8 mod 5 = 3, linking the triplet structure to the number 8 from the recognition cycle. The charged pion is proved heavier than the neutral one, with the mass difference within 0.1 MeV of 4.6 MeV, and the relative difference is about 3.4 percent.

The framework's contribution is a placement, not a derivation from first principles. The φ-ladder placement is a model that organizes known masses, and the numerical agreements are empirical checks. The module does not derive the pion mass from the forcing chain; it uses measured values as definitions and proves consistency relations around them.

/-- Pion mass is around 140 MeV. -/
theorem pion_mass_near_140 : abs (pionChargedMass_MeV - 140) < 1 := by
  simp only [pionChargedMass_MeV]
  norm_num

/-- π⁺ is heavier than π⁰ (electromagnetic mass difference). -/
theorem charged_heavier_than_neutral : pionChargedMass_MeV > pionNeutralMass_MeV := by
  simp only [pionChargedMass_MeV, pionNeutralMass_MeV]
  norm_num

/-- Mass difference is about 4.6 MeV (electromagnetic). -/
theorem mass_difference_electromagnetic :
    abs (pionMassDifference_MeV - 4.6) < 0.1 := by
  simp only [pionMassDifference_MeV, pionChargedMass_MeV, pionNeutralMass_MeV]
  norm_num

/-- Pion-electron mass ratio is approximately 273. -/
theorem pion_electron_ratio_approx : abs (pionElectronRatio - 273) < 1 := by
  -- pionChargedMass_eV / electronMass_eV = (139.57039 × 1e6) / (0.51099895 × 1e6) ≈ 273.13
  -- |273.13 - 273| = 0.13 < 1
  simp only [pionElectronRatio, pionChargedMass_eV, pionChargedMass_MeV, electronMass_eV]
  norm_num

theorem relative_difference_about_3_percent :
    abs (relativeMassDifference - 3.4) < 0.1 := by
  -- ((139.57039 - 134.9768) / 134.9768) * 100 = (4.59359 / 134.9768) * 100 ≈ 3.403
  -- |3.403 - 3.4| = 0.003 < 0.1
  simp only [relativeMassDifference, pionMassDifference_MeV, pionChargedMass_MeV, pionNeutralMass_MeV]
  norm_num

What this page does not claim

The pion mass is not derived from the forcing chain; it is placed on a φ-ladder as a model. The ratio m_π/m_e ≈ φ¹² / 2 is a numerical coincidence, not a proved equality. The GMOR relation is not proved by the framework; only a sanity bound on its prediction is checked.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/PionMasses.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: