kShortLifetime
plain-language theorem explainer
The declaration assigns the short-lived neutral kaon lifetime the value 8.954e-11 seconds. Kaon physicists and Recognition Science modelers cite this constant when computing the K_L/K_S decay ratio and checking phi-ladder mass predictions against data. It enters the module as a bare numerical definition with no internal lemmas or reduction steps.
Claim. The lifetime of the short-lived neutral kaon $K_S$ equals $8.954 times 10^{-11}$ seconds.
background
The Kaon Masses module derives properties of strange mesons (K^+, K^0 and conjugates) that contain one strange quark or antiquark. Their placement on the phi-ladder follows from the heavier strange-quark mass dominating over light quarks, producing mass ratios near phi^2.6 and the observed charged-neutral splitting opposite to the pion case. The module imports Constants, PhiForcing, and PionMasses to anchor these ratios in the Recognition Composition Law and the eight-tick octave structure.
proof idea
The entry is a direct numerical definition that assigns the experimental K_S lifetime without invoking any upstream lemmas or tactics.
why it matters
This constant is referenced by the lifetime_ratio theorem, which verifies that the K_L/K_S ratio lies within 1 of 571. It supplies the lifetime datum required by the P-014 kaon derivation, linking the phi-ladder mass formula to CP-violation observables in the neutral kaon system. The definition closes the numerical interface between the RS mass ladder and measured weak-decay rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.