kShortMass_MeV
plain-language theorem explainer
The definition supplies the short-lived neutral kaon mass K_S as the constant 497.611 MeV drawn from Recognition Science kaon predictions. Physicists modeling neutral kaon mixing or testing phi-ladder mass ratios would cite this value to anchor comparisons with measured decay rates. It is realized as a direct real-number assignment with no lemmas or computational steps.
Claim. The short-lived neutral kaon mass equals $m_{K_S} = 497.611$ MeV.
background
The Kaon Masses module derives masses for strange mesons (K^+, K^-, K^0, Kbar^0) containing one strange quark or antiquark. Recognition Science places these particles on a higher rung of the phi-ladder than pions because the strange quark mass near 95 MeV dominates the light-quark contributions, producing mass ratios that follow phi-patterns such as m_K/m_pi near phi^2.6. The module states the explicit prediction K^0 mass near 497.61 MeV, which this definition matches for the short-lived neutral state.
proof idea
The declaration is a direct numerical definition that assigns the real constant 497.611 to the K_S mass in MeV units, with no lemmas applied and no tactics required.
why it matters
This definition anchors the numerical values in the P-014 kaon mass derivation and supports sibling quantities such as kaon mass differences and kaon-pion ratios. It realizes the Recognition Science mass formula on the phi-ladder for neutral kaons, consistent with the framework landmarks of T6 self-similar fixed point and the eight-tick octave. No open questions are closed by this entry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.