kaonMassDifference_MeV
plain-language theorem explainer
The declaration defines the mass difference between neutral and charged kaons in MeV. Particle physicists applying Recognition Science to meson spectra would cite it when checking the strange-quark-induced splitting against data. The definition is a direct subtraction of two real constants fixed to PDG 2024 values.
Claim. The kaon mass difference in MeV is defined by $m_{K^0} - m_{K^+} $, where $m_{K^0}$ and $m_{K^+}$ are the neutral and charged kaon masses.
background
The module derives kaon masses from Recognition Science by placing the strange quark on a higher rung of the phi-ladder than the light quarks in pions. Kaons are treated as strange mesons (K⁺ = u s̄, K⁰ = d s̄) whose masses are dominated by the strange-quark contribution near 95 MeV. Mass is the type alias for real numbers in RS-native units. The charged and neutral masses are supplied as fixed constants 493.677 MeV and 497.61 MeV drawn from PDG 2024 tabulations.
proof idea
This is a definition that subtracts the charged-kaon constant from the neutral-kaon constant. No lemmas or tactics are applied beyond the two upstream mass definitions.
why it matters
It supplies the exact difference used by the downstream approximation theorem that verifies the splitting lies within 0.1 MeV of 3.9. The declaration fills the numerical step in the P-014 kaon-masses derivation, supporting the phi-ladder placement for strange quarks and the predicted reversal of charged-neutral ordering relative to pions. It connects to the Gell-Mann-Okubo mass formula cited in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.