Physics Kaon Masses

Kaon masses

The kaons are four mesons, particles made of one quark and one antiquark, that contain a strange quark or its antiparticle. The charged kaons K⁺ and K⁻ weigh about 493.68 MeV, and the neutral kaons K⁰ and K̄⁰ about 497.61 MeV, where MeV is a standard particle-physics energy unit. The neutral kaon is slightly heavier than the charged one, opposite to the pattern in pions, because the strange quark's electromagnetic effects shift the balance. These particles also have famously different lifetimes: the long-lived neutral kaon survives about 5.116 × 10⁻⁸ seconds, while the short-lived one decays in about 8.954 × 10⁻¹¹ seconds, a ratio near 571.

Kaon physics has a long classical history. Murray Gell-Mann and Kazuhiko Nishijima independently proposed strangeness in 1953 to explain why kaons are produced strongly but decay weakly. The Gell-Mann-Okubo mass formula, from 1962, relates the masses of the pseudoscalar meson octet: four times the kaon mass squared approximately equals three times the eta mass squared plus the pion mass squared. The neutral kaon system also displays CP violation, the slight asymmetry between matter and antimatter that was discovered in 1964 by James Cronin and Val Fitch, a result that helped explain why the universe contains more matter than antimatter.

In Recognition Science, the kaon masses are not free parameters but consequences of the framework's forcing chain. The framework models the strange quark mass at 93.4 MeV and places kaons on a higher rung of its phi-ladder than pions, because the strange quark is heavier than the up and down quarks. The mass ratio m_K/m_π is approximately 3.54, which the framework identifies as close to φ^2.6, where φ is the golden ratio, about 1.618. The framework's machine-checked library of formal theorems proves that this ratio lies within 0.01 of 3.54, that the neutral kaon is heavier than the charged one, and that the mass difference between them is within 0.1 MeV of 3.9 MeV. The library also proves the Gell-Mann-Okubo relation holds to within 10 percent, and that the kaon-to-pion mass ratio is within 0.1 of φ² + 0.9.

These are not derivations of the masses from first principles. The framework defines the kaon masses as numbers, then proves proximity theorems about them. The kaon mass values themselves are inputs, chosen to match measurements, not outputs of the forcing chain. What the framework establishes is that these measured values sit on a phi-powered ladder consistent with its structure, and that classical relations like Gell-Mann-Okubo hold within the framework's tolerance. The framework's contribution is a structural pattern, not a prediction of the masses from nothing.

/-- Kaon-pion mass ratio is approximately 3.54. -/
theorem kaon_pion_ratio_approx : abs (kaonPionRatio - 3.54) < 0.01 := by
  -- 493.677 / 139.57039 ≈ 3.5372
  -- |3.5372 - 3.54| = 0.0028 < 0.01
  simp only [kaonPionRatio, kaonChargedMass_MeV, pionChargedMass_MeV]
  norm_num

/-- K⁰ is heavier than K⁺ (opposite to pions). -/
theorem neutral_heavier_than_charged : kaonNeutralMass_MeV > kaonChargedMass_MeV := by
  simp only [kaonNeutralMass_MeV, kaonChargedMass_MeV]
  norm_num

/-- Mass difference is about 3.9 MeV. -/
theorem kaon_mass_difference_approx :
    abs (kaonMassDifference_MeV - 3.9) < 0.1 := by
  simp only [kaonMassDifference_MeV, kaonNeutralMass_MeV, kaonChargedMass_MeV]
  norm_num

theorem gmo_relation_approximate :
    abs (gmo_lhs - gmo_rhs) / gmo_lhs < 0.1 := by
  -- gmo_lhs = 4 × 493.677² ≈ 974867
  -- gmo_rhs = 3 × 547.862² + 139.57039² ≈ 919947
  -- Difference ≈ 54920, ratio ≈ 0.056 < 0.1
  simp only [gmo_lhs, gmo_rhs, kaonChargedMass_MeV, etaMass_MeV, pionChargedMass_MeV]
  norm_num

What this page does not claim

The kaon masses are derived from first principles; they are defined values that the framework places on a phi-ladder. The framework predicts the exact kaon mass values; it proves proximity relations to phi-based expressions and classical formulas. The framework's CP violation treatment is a full model of the neutral kaon system; it references the phenomenon without deriving its magnitude.

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/KaonMasses.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: