kLkS_massDifference
plain-language theorem explainer
The declaration assigns the fixed numerical value 3.484e-12 MeV to the K_L minus K_S mass difference. Particle physicists modeling neutral kaon mixing or CP violation within the Recognition Science framework cite this constant when scaling decay spectra or mass splittings on the phi-ladder. It is introduced by direct real-number assignment with no computation or reduction steps.
Claim. The mass difference between the long-lived and short-lived neutral kaons satisfies $m_{K_L} - m_{K_S} = 3.484 × 10^{-12}$ MeV.
background
Kaon masses are derived in Recognition Science from strange-quark content and phi-ladder placement. The module states that kaons occupy a higher rung than pions because the strange quark mass dominates, producing the observed mass ratio m_K/m_π ≈ φ^2.6 and the reversal K^+ < K^0 relative to the pion ordering. The upstream definition lifetime(k) := phi^k supplies the exponential scaling used for decay spectra that contextualizes the small K_L-K_S splitting arising from weak-interaction CP violation.
proof idea
The definition is a direct constant assignment of the experimental mass-difference value in MeV units.
why it matters
This constant supplies the numerical input required by the Kaon Masses Derivation (P-014) for the neutral-kaon system. It anchors the CP-violation phenomenology to the phi-ladder and the eight-tick octave structure while remaining consistent with the Gell-Mann-Okubo mass formula inside the RS framework. No downstream theorems are listed, so the constant functions as a boundary datum rather than an internal derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.