kLongMass_MeV
plain-language theorem explainer
The long-lived neutral kaon mass is fixed at 497.611 MeV. Kaon phenomenology groups reference this constant when computing lifetimes or CP-violating parameters. It appears as a direct numerical definition matching the predicted neutral kaon mass from the phi-ladder.
Claim. The mass of the long-lived neutral kaon $K_L$ is $497.611$ MeV.
background
Kaons are strange mesons containing one strange quark or antiquark, with the strange quark mass dominating over light quarks. The module places kaons on a higher rung of the phi-ladder than pions, producing mass ratios near phi to the power 2.6 and invoking SU(3) flavor symmetry plus CP violation in the neutral system. The local setting derives kaon masses from Recognition Science, with the explicit prediction that the neutral kaon mass is approximately 497.61 MeV.
proof idea
The definition directly assigns the numerical value 497.611 as a bare constant, consistent with the K^0 mass prediction stated in the module.
why it matters
This constant anchors the neutral kaon sector and supports downstream calculations of mass differences and ratios such as kaonPionRatio. It implements the prediction K^0 mass ≈ 497.61 MeV from the RS mechanism in the phi-ladder. The entry closes the numerical input for kaon phenomenology within the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.