Pricing the Risk of Runtime Compression: Anytime-Valid Admission and a Served-Output Law for Compressed Serving State

TL;DR - This paper introduces formally verified, anytime-valid risk accounting for dynamically compressing LLM serving state. On live traffic, it maintained guarantees across 352,333 admission decisions and reduced exact fallbacks from 30% to 14% at matched risk.

• Replaces request-level union bounds—which exhausted on every long request—with a physically accounted risk ledger valid at every admission call.
• Derives a machine-checked law linking served-output total variation to a configurable compression threshold.
• Audits a 1,064× certification gap and attributes nearly all of it to the gate’s operating point rather than query-envelope looseness.
• Uses exchangeable order-statistic bounds across 80 serving histories for non-vacuous extrapolation; 228 probabilistic theorems are checked in Lean 4 without sorry.