lifetime_ratio
plain-language theorem explainer
The declaration verifies that the absolute difference between the ratio of long-lived to short-lived neutral kaon lifetimes and 571 is less than 1. Particle physicists modeling CP violation and decay spectra would cite this bound as a numerical check. The proof reduces directly to unfolding the two lifetime constants and applying numerical normalization.
Claim. $|K_L / K_S - 571| < 1$, where $K_L$ and $K_S$ are the lifetimes of the long-lived and short-lived neutral kaons.
background
Kaons occupy a higher rung on the phi-ladder than pions because of their strange-quark content, with the module placing $m_K/m_π ≈ φ^{2.6}$. The local setting derives masses and lifetimes from Recognition Science via the strange-quark mass scale and SU(3) octet relations, while noting $K_L$-$K_S$ mixing as a CP-violation signature. Upstream, the dimensionless bridge $K$ is defined as $φ^{1/2}$ and Tick structures supply the discrete eight-tick clock that governs temporal progression in the framework.
proof idea
One-line wrapper that applies simp only on the constants kLongLifetime and kShortLifetime, then norm_num to confirm the ratio lies within the integer tolerance of 571.
why it matters
The result supplies the phi_ratio field inside decaySpectrumCert, which certifies the full decay spectrum constructed from the phi-ladder. It anchors the kaon sector to the T7 eight-tick octave and the mass formula yardstick · φ^(rung-8+gap(Z)). The module treats neutral-kaon CP violation as an intrinsic RS feature rather than an added hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.