kLongLifetime
plain-language theorem explainer
The declaration supplies the numerical value 5.116e-8 for the long-lived neutral kaon lifetime in seconds. Particle physicists modeling kaon decays or CP violation within Recognition Science cite this constant when forming lifetime ratios or decay spectra. It enters as a direct numerical assignment chosen to match observed data rather than computed from phi-ladder scaling in the module body.
Claim. The lifetime of the long-lived neutral kaon $K_L$ equals $5.116 times 10^{-8}$ seconds.
background
The Kaon Masses module derives strange-meson properties from Recognition Science by placing kaons on a higher rung of the phi-ladder than pions, reflecting the dominant strange-quark mass contribution and SU(3) octet structure. The upstream lifetime definition from DecaySpectrumFromPhiLadder sets lifetime k equal to phi raised to the power k, supplying the exponential scaling law for decay times. Module documentation notes that neutral-kaon CP violation and the Gell-Mann-Okubo mass splitting are incorporated as consequences of this placement.
proof idea
This declaration is a direct numerical definition that hardcodes the real number 5.116e-8. It does not invoke the upstream lifetime function or apply any lemmas or tactics inside its body.
why it matters
The constant feeds the lifetime_ratio theorem, which verifies that the K_L to K_S ratio lies within 1 of 571. It supplies the experimental anchor required by the P-014 kaon-mass derivation and aligns with the phi-ladder scaling and eight-tick octave from the T5-T8 forcing chain. No open scaffolding questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.