Paper deep dive
Pricing the Risk of Runtime Compression: Anytime-Valid Admission and a Served-Output Law for Compressed Serving State
Fanzhe Wei, Li Liu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 8/22/2026, 3:05:24 AM
Summary
This paper introduces a machine-checked framework for pricing the risk of runtime compression in serving state, specifically for Mixture of Experts (MoE) models. It replaces union-bound admission controls with an anytime-valid, physically-accounted ledger that holds across 352,333 live admission calls, halving the exact-fallback rate from 0.30 to 0.14 at matched risk. The authors derive a 'Served-Output Law' (TV <= tanh(a_q w_thr)) to quantify the gap between certified witnesses and user experience, localizing a 1064x gap to the gate's operating point. Finally, they use exchangeable extrapolation across 80 serving histories to provide order-statistic bounds for unseen requests, replacing vacuous conformal prediction certificates. All probabilistic kernels are verified in Lean 4.
Entities (13)
Relation Signals (8)
Metask Lab → affiliationof → Fanzhe Wei
confidence 99% · Fanzhe Wei Affiliation: Metask Lab
Metask Lab → affiliationof → Li Liu
confidence 99% · Li Liu Affiliation: Metask Lab
Lean 4 → verifies → probabilistic kernels
confidence 96% · All probabilistic kernels are Lean 4-checked (228 exported theorems, no sorry)
Anytime-Valid Admission Ledger → replaces → Union Bound
confidence 95% · We show the union budget exhausts on every long request... and replace it with an anytime-valid, physically accounted ledger
Anytime-Valid Admission Ledger → reduces → exact-fallback rate
confidence 94% · halves the exact-fallback rate at matched risk (0.30 -> 0.14)
Served-Output Law → quantifies → gap between certified witness and user experience
confidence 93% · a machine-checked design law (TV <= tanh(a_q w_thr)) turns the served-TV target into a threshold knob... localizes the entire 1064x gap
Exchangeable Extrapolation → replaces → Conformal Prediction
confidence 92% · exchangeable extrapolation across 80 serving histories replaces binary conformal prediction's vacuous certificates
DeepSeek-V2-Lite → demonstrates → routing margin vulnerability
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Runtime compression of serving state trades quality for capacity with no priced guarantee: systems adapt precision on load signals with no soundness statement, and certified approaches budget request-level risk by a union bound over a pre-declared event count. We show the union budget exhausts on every long request in a production serving stack (100% of requests), and replace it with an anytime-valid, physically accounted ledger whose bound holds at every one of 352,333 admission calls on live traffic and which, in a pre-registered held-out confirmatory round, halves the exact-fallback rate at matched risk (0.30 -> 0.14) -- coverage is bought at a price the account states. We then price the remaining distance from the certified witness to what a user experiences: a machine-checked design law (TV <= tanh(a_q w_thr)) turns the served-TV target into a threshold knob, and a three-layer audit of its instantiation -- an operator-norm query envelope measured 1.5x from tight, a measured-ellipsoid replacement for the Cauchy-Schwarz ball that buys nothing (0.89x, held-out sound), and the gate's operating point (~700x) -- localizes the entire 1064x gap to the operating point, a price the law now states rather than an unknown. A priced bound is worth nothing on a request one has not seen, so the third link is the quantifier: exchangeable extrapolation across 80 serving histories replaces binary conformal prediction's vacuous certificates with order-statistic bounds that discriminate (0.41 against 0.51 calibration risk). All probabilistic kernels are Lean 4-checked (228 exported theorems, no sorry); which object deserves this machinery at all is settled empirically in a companion paper that adjudicates -- and rejects -- the natural alternative of certifying routing. What ships is an account: risk you can spend, a gap you can read off a law, and a bound that survives the request you have not seen.
Tags
Links
- Source: https://arxiv.org/abs/2608.15810v1
- Canonical: https://arxiv.org/abs/2608.15810v1
Trouble viewing inline? Open PDF directly →
Full Text
100,973 characters extracted from source content.
Expand or collapse full text
Pricing the Risk of Runtime Compression: Anytime-Valid Admission and a Served-Output Law for Compressed Serving State Fanzhe Wei Affiliation: Metask Lab Email: whyer1@gmail.com Li Liu Affiliation: Metask Lab Email: muriel092611@gmail.com Abstract Runtime compression of serving state trades quality for capacity with no priced guarantee: systems adapt precision on load signals with no soundness statement, and certified approaches budget request-level risk by a union bound over a pre-declared event count. We show the union budget exhausts on every long request in a production serving stack (100%100\% of requests), and replace it with an anytime-valid, physically-accounted admission ledger whose bound holds at every one of 352,333352,333 admission calls on live traffic and which, in a pre-registered held-out confirmatory round, halves the exact-fallback rate at matched risk (0.30→0.140.30→ 0.14) — coverage is bought at a price the account states. We then price the remaining distance from the certified witness to what a user experiences: a machine-checked design law (TV≤tanh(aqwthr)TV≤ (a_qw_thr)) turns the served-TV target into a threshold knob, and a three-layer audit of its instantiation — an operator-norm query envelope measured 1.5×1.5× from tight, a measured-ellipsoid replacement for the Cauchy–Schwarz ball that buys nothing (0.89×0.89×, held-out sound), and the gate’s operating point (∼700× \!700×) — localizes the entire 1064×1064× gap to the operating point, a price the law now states rather than an unknown. A priced bound is still worth nothing on a request one has not seen, so the third link is the quantifier: exchangeable extrapolation across 8080 serving histories replaces binary conformal prediction’s vacuous certificates with order-statistic bounds that discriminate (0.410.41 against 0.510.51 calibration risk). All probabilistic kernels are Lean 4-checked (228228 exported theorems, no sorry); which object deserves this machinery at all is settled empirically in a companion paper (What to Protect When You Quantize a Mixture of Experts) that adjudicates — and rejects — the natural alternative of certifying expert routing. What ships is an account: risk you can spend, a gap you can read off a law, and a bound that survives the request you have not seen. Figure 1: The chain this paper machine-checks, and where it stops. Solid boxes and their connecting theorems are proved in Lean with no sorry; dotted boxes are measured or open. Reading left to right: a per-step moment bound on the rounding draw becomes a bound on expected served-output total variation, Bernoulli domination feeds it to the anytime ledger, and Ville’s inequality closes the request. The lower row is the quantifier: exchangeable history sampling lifts a fixed-history bound to an unseen history, and the one box we cannot fill is that our population is a pool we constructed rather than runtime traffic. The propagation constants that a tensorized proof would need are measured and falsified, not bounded — which is why the top row is stated for an arbitrary step perturbation. 1 Introduction Quantization for large-model serving is decided at the wrong timescale. Post-training quantization chooses a static configuration offline and defends it with average-case evidence; serving systems increasingly change precision at runtime (layer swapping under memory pressure, learned bit-plane routing, phase-split precision) with no soundness statement. The structural gap: no system decides precision from the content of the current request while providing a sound, per-request accounting of the risk that decision incurs. For MoE models the gap is sharper: quantization error also flips discrete routing decisions (on Mixtral-8×7B at extreme compression, expert selection changes on over 40%40\% of tokens — GEMQ [3]), and the published response is entirely offline. Our own measurement sharpens the point: quantizing the router itself to INT4 flips 63.2%63.2\% of top-6 selections on DeepSeek-V2-Lite, because the quantity a routing certificate would protect is an order of magnitude smaller than the noise it would have to survive: med(s(k)−s(k+1))⏟routing margin=0.023≪2Lmed(ε∞)⏟gate noise=0.354(L=1). med (s_(k)-s_(k+1) )_routing margin=0.023\; \; 2L\,med( _∞)_gate noise=0.354 (L=1). (1) This explains, with numbers, a practice the industry adopted by instinct (production MXFP4 checkpoints exclude mlp.gate without exception) — and it identifies the quantity an online certificate must protect: the margin between the k-th and (k+1)(k+1)-th routing logits against upstream precision noise. This paper prices runtime compression of serving state. The account is one chain — an object, its price, and the quantifier that decides whether the price means anything on the request not yet seen — and we state for each link both what it buys and where it stops: • The object: a risk that can actually be spent. Prior certified systems budget per-event failure by union bound and state that no union bound survives free-running decoding. The tempting fix — let the e-process itself admit actions — changes the guarantee’s object (it controls wrongly rejecting an honest radius model, not admitted-action failure; we give the exact counterexample). We close the sound branch instead: a machine-checked anytime-valid budget on cumulative realized loss (cumloss_admission) whose per-event terms the write-path audit already measures (§4). • The price: what one unit of that risk buys a served token. A machine-checked chain carries the witness’s per-layer variance budget to a request-level served-TV tail bound (request_tail_of_served_tv), and a design law turns the served-TV target into a threshold knob; a three-layer audit of that law’s instantiation localizes the entire 1064×1064× gap between the certified witness and the served output to the gate’s operating point — a price the law now states rather than an unknown (§5, §7). Open and stated as such: the model-side propagation constants (measured, and the measurement falsifies the first-order surrogate) and the live controller beyond its +3.8%+3.8\% judgment cost. • The quantifier: whether any of it holds on the next request. A bound calibrated on the histories one happens to have is not yet a bound on the history about to be served. Exchangeable without-replacement sampling over 8080 serving histories lifts it and replaces binary conformal prediction’s vacuous certificates with order-statistic bounds that discriminate (0.410.41 against 0.510.51 calibration risk, §6). The premise we cannot supply is that our population is a pool we constructed rather than runtime traffic; we say so wherever the number is used. Two things this paper deliberately does not do. It does not certify expert routing: that alternative object we built first and rejected on measured grounds, an adjudication that is the companion measurement paper’s subject11 1 Companion measurement paper, What to Protect When You Quantize a Mixture of Experts, by the same authors, posted concurrently. No result of that paper is claimed here, and this paper is self-contained without it. and none of whose results are claimed here — §3 states only the boundary it draws, which is why the object priced above is the served output rather than the routing decision. And it does not bury the kill-shots that shaped the design: the gate-quantization arm above, and the pre-registered death of a value-transport rescue hypothesis for KV quantization (synthetic pool: rank correlation 0.8720.872, zero rescuable condemned reads; real-pool recheck: the production quantizer family never reaches the condemnation stratum, adjudicated “inconclusive, no high shift”, metric-to-error correlation 0.9350.935), which redirected this paper from KV distortion metrics to precision decisions. Separately, the precondition study for request-conditioned geometry — which no bound in this paper consumes — is reported in Appendix B rather than claimed as a result. Model Routing Experts / top-k Layers Where it carries the paper DeepSeek-V4-Flash-FP8 sqrtsoftplus, bias-corrected 256256 / 66 4343 served-output bridge; anytime ledger; physical gate; 8080-history conformal extrapolation GLM-5.2 (FP8, W4A-FP8) sigmoid, bias-corrected 256256 / 88 7878 capacity–cost evaluation in the production stack DeepSeek-V2-Lite softmax, greedy 6464 / 66 2727 router-margin certificate; flip→ arms Qwen1.5-MoE-A2.7B softmax, greedy 6060 / 44 2424 cross-model replication of the flip arms Qwen2.5-7B dense — 2828 activation-geometry precondition (dense control) Table 1: Model coverage. The served-output line runs on a production-scale fine-grained MoE (256256 experts, top-66); the capacity evaluation on a second, architecturally distinct one; the routing-certificate arms on smaller greedy-top-k MoEs, treated as a same-family proxy (§3). Scope of the controlled action, stated up front. Table 1 lists which model carries which result. The admission engine is object-agnostic — its inputs are audited per-event losses and predictable MGF terms, whichever component produces them — but the action it controls in this paper is KV-write precision (dithered compression vs. exact retention) inside an MoE serving stack. Expert-weight precision actions — the switch whose economics §A measures at 3.73×3.73× capacity headroom — are the engine’s designated next object, not a delivered one. We price that headroom rather than quote it: pressure-probed at 2626k-token requests it converts to 2.02.0–2.24×2.24× the in-flight requests, and from there to nothing when prefixes never repeat and to 1.19×1.19× throughput (a measured lower bound) when each session reuses its own context (Table 8); which it becomes is decided by the workload, and we report both. The switch itself — per-component weight-plane management — is motivated here, not implemented: an engine proved on the first object, the second object’s value quantified and its mechanism left open. Everything is measured under a provenance-stamped, machine-adjudicated protocol: every gate in this paper was pre-registered with its verdict branches written before the data was seen, and every number traces to a run artifact. Table 10 is the full ledger of those branches and the verdict each one fired. 2 Setup and inherited contracts We inherit the typed-contract vocabulary of our prior systems (WitCert [15] and its observability companion [14]): typed input/output metrics with mismatch rejection; certified / partial / empirical tiers; per-request ledgers; and machine-checked (Lean 4) soundness for the probabilistic kernel. Notation: a serving process emits memory/compute events t=1,2,…t=1,2,… with filtration (ℱt)(F_t); a precision plan assigns each linear component ℓ an action aℓa_ (bit-width, exact-keep, or fallback); request-level risk is budgeted as δreq _req. The whole paper turns on one structural requirement, which we state once and then never relax: at∈ℱt−1,Lt∈[0,1]isℱt-measurable,[Lt∣ℱt−1]≤μ.a_t _t-1, L_t∈[0,1]\ is\ F_t-measurable, [L_t _t-1 ]≤μ. (2) Decisions must be predictable — chosen before the loss they incur is revealed — because an anytime bound over a stream that adapts to its own outcomes is otherwise not a bound at all. 2.1 What is inherited and what is new Sound runtime certificates for KV-cache quantization exist (ours and independent work); request conditioning, sound per-read bounds, and serving-loop evidence are established there for the KV domain, and we do not re-claim them. This paper’s claims live strictly in the two vacant axes: anytime-valid budgets that drive decisions, and the online MoE routing question — the latter adjudicated negatively in the companion paper (§3). An ellipsoid radius conditioned on the request would need activations to concentrate in low-dimensional subspaces; we test that precondition with held-out controls and report it in Appendix B, since no bound in this paper consumes it. 3 What not to certify: the routing adjudication, in brief A natural first candidate for the certified object is expert-routing invariance, and we built that certificate before pricing it: a sound selection-domain margin test with per-model Lipschitz constants, adjudicated across nine MoE families (485,138485,138 tokens, zero soundness violations). The verdict, reported in full in the companion measurement paper, is negative on three independent grounds — the gate binds on 9494–100%100\% of production traffic and remains unusable after every sound tightening we could construct (including a measured per-coordinate ellipsoid); the flips it prevents anti-predict damage; and set identity provably fails to bound the routing distribution it was meant to protect. Replaying full-precision routing recovers a constant 88–17%17\% of quantization damage across every knob the companion paper turns, worth 0.75%0.75\% of base perplexity at the four-bit depth production ships, and becomes actively harmful past a model-dependent damage cliff. We therefore take the routing question as settled against certification and spend this paper on the object the adjudication points to: the served output’s cumulative tail under a request-level risk budget, which the rest of this paper defines, prices, and machine-checks. 4 Anytime-valid admission Certified systems to date spend request-level risk by union bound over a pre-declared event count: δt=δreq(t+1)(t+2),∑t≥0δt=δreq, _t\;=\; _req(t+1)(t+2), _t≥ 0 _t\;=\; _req, (3) which is sound but pays for horizon in advance. Our own prior system states the limitation precisely: free-running decoding feeds quantized cache back into future queries, an adaptive dependence “no union bound repairs”; its e-process was deployed only as model validation, “complementing, not replacing” the union budget that authorization consumes. The tempting construction — admission gated by the e-process wealth itself — is the one we implemented first, and it is wrong for the stated guarantee. Ville’s inequality bounds the probability that an honest radius model ever looks anomalous; it says nothing about the probability that an admitted action fails. The two differ by more than a constant. A 2,0002,000-event stream admitted at per-event risk 10−410^-4 passes the wealth test while incurring an 18%18\% any-failure probability, so wealth-gating answers a question nobody asked. The corrected object is a budget on cumulative realized loss, and its admission rule is machine-checked (cumloss_admission): if the account is maintained at rate λ with the per-event terms the write-path audit already produces, then Pr(∃t≤T:∑s≤tLs>Bt)≤δ (∃ t≤ T: _s≤ tL_s>B_t)≤δ. Two facts make this implementable rather than aspirational. The gate is conservative in the right direction — admitting on batch-level upper bounds while settling on the subset that actually passes preserves the budget (gating_conservative) — and at the request endpoint the certified account is tight against the physical witness it charges rather than orders of magnitude loose (median margin of bound over witness 4.6%4.6\% across 1616 endpoints, witness below bound on all of them). That is an endpoint statement about accumulated totals: the run does not record a per-event margin trajectory, so individual events may run looser and offset. union cumloss, by budget B~ B ×1035\!×\!10^3 ×1042\!×\!10^4 ×1045\!×\!10^4 budget exhaustion 100%100\% — — — fallback-to-exact rate (median) 0.3150.315 0.8420.842 0.3390.339 0.00790.0079 admission calls (armed) 00 641,284641,284 1,336,5881,336,588 — judgment cost (s/request) 344.5344.5 339.5339.5 357.1357.1 — violations 00 00 00 00 Table 2: Dual-accounted admission, measured in a production serving stack. The union budget exhausts on every long request; cumulative-loss admission does not — what it buys is a monotone coverage/budget curve, not a free lunch, and each column must be read at its own budget: at B~=×104 B=2\!×\!10^4 the fallback rate (0.3390.339) is worse than the union baseline’s 0.3150.315, and the pre-registered mechanism control recorded exactly that, so that arm’s adjudication is reported INVALID rather than quoted as a win. The 31.49%→0.79%31.49\%\!→\!0.79\% drop is real but belongs to the 2.5×2.5× wider budget B~=×104 B=5\!×\!10^4. Zero authorization violations across all arms. Full adjudication notes (cross-run calibers, non-monotone judgment cost, physical-gate non-vacuity) in Appendix F. Figure 2: Coverage is bought, not found. Fallback-to-exact rate vs. cumulative-loss budget (exploratory normalized-z arm), union baseline for reference: at Table 2’s budget the cumulative account is worse than union; the large gain belongs to a 2.5×2.5× wider budget. We then close the loop: a physical-gate armed run (WITCERT_CUMLOSS_MODE=phys, frozen commit, nine pre-registered gates all passing) drives KV-write admission by the physical account itself — 317,293317,293 and 352,333352,333 admission calls in the loose and tight arms. Three properties hold on live data. The physical anytime bound is never crossed: per account, at every admission call, maxt(realized charget−admitted charget)≤ 0, _t\; (realized charge_t-admitted charge_t )\;≤\;0, (4) the L=WL=W instantiation of cumloss_admission realized, and the runtime counterpart of gating_conservative and admit_implies_realized_within — admitting on the full-batch upper bound is provably safe per step, here measured account-by-account. The controller modulates by budget (tight exact-fallback 0.480.48 vs. loose 0.220.22 against the same round’s union baseline 0.310.31). And in a pre-registered held-out confirmatory round (frozen λ and budget, topic-disjoint), all three properties replicate and the coverage gain becomes a same-round comparison: physical arm 0.140.14 vs. its own union 0.300.30. Not recorded: the margin trajectory maxt(realizedt−prospectivet) _t(realized_t-prospective_t) — the zero-violation fact says only that the conservatism’s slack is non-negative. The judgment costs +3.8%+3.8\% wall time. Two honest caveats remain. λ and the budgets were calibrated in one exploratory round and confirmed in one frozen held-out round — a single replication, not a sweep; and W is a local certified witness (band-norm of K/V residual), not served TV/NLL. The served-output leg has a three-part status. Per read it is sound: the inherited machine-checked tv_le_eform bounds one attention softmax’s TV by 12(Ac2−1) 12(A_c^2-1). Soundness is not usefulness (Figure 3): reconstructed on captured reads the bound exceeds 11 — certifies nothing — on 6.7%6.7\% of reads at m=2m=2 masked mantissa bits, 41.8%41.8\% at m=3m=3, 92.9%92.9\% at m=4m=4; a worst-key probe returns “TV≤1.54TV≤ 1.54”. Each read carries a valid certificate, not always an informative one. Figure 3: Valid is not the same as informative. Fraction of captured reads on which each per-read bound exceeds 11 (certifies nothing) as mantissa bits are masked: the inherited e-form degrades from usable to useless; the gate tanh law of (18) stays non-vacuous. This measurement motivated replacing the bound, not post hoc. Cumulatively the naive obstacle — total variation does not add across reads and layers — dissolves: what adds is the output-logit perturbation, because the residual stream is additive, so the whole request’s served TV is one tanh over a sum of per-layer bounds (cumulative_output_tv, developed with the measurement in §6 and (21)). Empirically, per-read attention-distribution shift and per-read output error move together on real pools (Spearman 0.9350.935 — an ordering statement, not a magnitude one, on the attention leg); it motivates the pre-registered target for a sound per-layer bound, and is not evidence that the sum is small. The expert-weight action is the same shape of open work. Figure 4: Escaping the ℓ∞ _∞ wall. The cumulative served total variation realized by the deployed compressor (top) against three sound upper bounds, per-request medians over eight requests on the armed model. The bound inherited from the per-read theory, tanh‖Δlogit‖∞ \| \|_∞, is vacuous at 0.9960.996: it prices the worst logit coordinate, which sits on a low-probability token. Total variation instead prices mass movement, and both a mass-overlap bound (Bhattacharyya, 0.1590.159) and a pure-variance bound (sub-Gaussian, 0.2300.230) are non-vacuous and machine-checked. All quantities come from the same verdict artifact as the prose. Caliber: these are computed post hoc from paired exact and compressed logits, so the figure certifies the geometry — which functional can bound realized served TV at all — not a certificate the online witness emits today; supplying the same bound from the witness alone is Theorem 1’s a-priori branch, whose open constant we state in §10. Theorem 1 (Per-step variance budget to request-level served risk). Let a request’s decoding steps be indexed by history h; let php_h be the exact served distribution at h and let the compressed step’s distribution be the tilt ph,ω′(v)∝ph(v)eδh(ω,v)p _h,ω(v) p_h(v)e _h(ω,v) induced by that step’s rounding draws ω (the whole per-step draw vector, whatever its internal structure). Assume, for every history h: (i) gauge, ∑vph(v)δh(ω,v)=0 _vp_h(v) _h(ω,v)=0 for every ω; (i) a per-coordinate moment bound ω[eδh(ω,v)]≤Bh(v)E_ω[e _h(ω,v)]≤ B_h(v), where writing Bh(v)=exp(bh(v)+sh(v)2/2)B_h(v)= (b_h(v)+s_h(v)^2/2) separates a deterministic bias bh(v)b_h(v) from a fluctuation proxy sh(v)2s_h(v)^2; (i) a uniform step budget μ with log∑vph(v)Bh(v)≤μ _vp_h(v)B_h(v)≤μ. Then the step loss obeys the mass-weighted bound ω[TV(ph,ph,ω′)]≤log∑vph(v)Bh(v)≤μ,E_ω [TV(p_h,p _h,ω) ]\;≤\; _vp_h(v)B_h(v)\;≤\;μ, (5) and if the ledger admits every step at rate λ>0λ>0 — i.e. the admission invariant (6) of cumloss_admission holds, log(1/δ)+∑s≤tlog(1+μ(eλ−1))λ≤Btfor every t, (1/δ)+ _s≤ t \! (1+μ(e^λ-1) )λ\;≤\;B_t every t, (6) which is what the controller checks before admitting — then the request-level guarantee (7) holds: for the whole request Pr(∃t≤T:∑s≤tTVs>Bt)≤δ. (∃\,t≤ T:\ _s≤ tTV_s>B_t )\;≤\;δ. (7) Proof (machine-checked). The statement is request_tail_of_served_tv_massweighted; its Doob-supplied root, taking bounded differences directly, is request_tail_of_served_tv_doob_massweighted. The argument — sub-Gaussian kernel, mass-weighted Jensen/Fubini step, and the Bernoulli domination (8) whose mean-one factor is what the anytime ledger consumes — is spelled out in Appendix C. Axioms are the three standard ones, no sorry. [eλTV]≤ 1+μ(eλ−1).E [e ]\;≤\;1+μ (e^λ-1 ). (8) 5 Instantiating the step budget The theorem above is a beam with two ends. This section supplies the left end — the per-step moment constant — through five routes, of which four failed and each failure is informative. Is the budget of the right order? Substituting one realized draw for Bh(v)B_h(v) gives 0.2300.230 (median over the 88 captured requests) against a realized served TV of 0.1180.118 — a realization, not a bound, but it places the object the theorem prices at the right order where the system runs; the three steps from there to a certificate are stated in Appendix D. Making the budget computable. The step budget ∑vph(v)Bh(v) _vp_h(v)B_h(v) is a sum over 129,280129,280 vocabulary terms per decoded token, which no serving path will pay — and does not have to: for any high-probability set S and tail envelope Bmax≥Bh(v)B_ ≥ B_h(v) for v∉Sv∉ S, ∑vph(v)Bh(v)≤∑v∈Sph(v)Bh(v)+(1−∑v∈Sph(v))Bmax, _vp_h(v)B_h(v)\;≤\; _v∈ Sp_h(v)B_h(v)+ (1- _v∈ Sp_h(v) )B_ , (9) so the O(|S|)O(|S|) right-hand side may be used in hypothesis (i) unchanged (massweighted_topk_bound, composed in request_tail_of_served_tv_topk); served distributions concentrate, so the tail mass multiplying BmaxB_ is small and the budget is spent on the tokens that carry the probability — a per-token evaluable bound. Instantiating the constants. What remains is to supply the theorem’s moment hypothesis for a real network. We tried five routes and kept the fifth; the ladder in Table 3 is the honest summary, and its shape carries a lesson we state once rather than four times. Route to the step budget What it prices Value Global Lipschitz envelope (weights) worst case over ℝdR^d 1022110^221 Local operator norm, as a supremum worst direction, rank 4242 σmax≈16.0 _ \!≈\!16.0 Per-layer, per-token empirical MGF assumes layer-local additivity 0.03900.0390 (model-dep.) Empirical Bernstein on it worst-case range ece^c 7.647.64 (vacuous) Joint scalar, betting CS the functional itself 0.03220.0322 on deployed rounding no surrogate 0.05520.0552 Table 3: Five routes to the same number (the surviving one shown at two operating points). The first four fail for one reason stated four ways: each prices a worst case — over inputs, over directions, over a modelling assumption, over a range — while the theorem asks for an expectation over rounding draws. The bounded differences behind rows three and four we did measure (cmax=3.81c_ =3.81, per-token, gauge-centred), and they are diagnostics, not budgets: rows three and four rest on layer-local additivity, which our own saturation measurement rejects. Only the fifth route — the last two rows — bounds the quantity the theorem consumes. The failures are informative. A global Lipschitz envelope is sound and hopeless: power iteration over all 4343 layers gives a stack envelope of 1022110^221 (median per-layer factor 1.39×1051.39× 10^5, largest spectral norm 387387), optimistic in three separate ways (power iteration lower-bounds the norm, RMSNorm omitted, experts sampled). Restricting to the region a request occupies buys a hundred orders of magnitude — formalized as a runtime-checkable containment obligation (bdd_diff_of_lipschitz_on, lip_iterComp_on) — but does not suffice as a supremum: the measured ratio’s dispersion puts the effective rank at 4242 of 1.37×1061.37× 10^6, lifting the operator-norm estimate to 16.016.0, 251×251× the typical ratio of 0.06380.0638. (We first read that typical ratio as a Lipschitz constant, which was wrong, and retract it.) Figure 5 shows the measurement that rules out the whole layer-local route — worst-case and typical alike. The resolution is not a sharper worst case. Fixing a history, resampling all layers jointly, and reducing each draw to the scalar Zj=∑vpveδ~j,vZ_j= _vp_ve δ_j,v removes the layer-local product, the union over 129,280129,280 tokens, and the per-layer accumulation of bias in one move. Better still, the ledger needs [TV]E[TV] rather than [Z]E[Z], and total variation lies in [0,1][0,1] deterministically, so a betting-style confidence sequence bounds it with no appeal to any sample extremum. That it is the same machinery the ledger runs on is not a slogan: the betting factor gh(x)=1+λh(m−x),λh≥0,g_h(x)=1+ _h(m-x), _h≥ 0, (10) is nonnegative by construction and has mean at most one under H0:m≤[X]H_0:m [X], so Ville’s inequality — the one already formalized for the ledger — bounds the probability that the capital ever crosses 1/δ1/δ (betting_factor_eprocess, betting_ucb_anytime). Inverting the test family built from (10) is what defines the bound, so its anytime coverage rests on a machine-checked argument rather than on a coverage simulation alone. The number: ω[TV]≤0.0322E_ω[TV]≤ 0.0322 at α=0.01α=0.01 over 279279 draws, against a realized mean of 1.25×10−51.25× 10^-5 (the scalar-moment route gives a point estimate of 0.00230.0023 on the same draws). The per-token cost is bounded too: enveloping the tail on the product pvBvp_vB_v rather than on BvB_v alone — the same anti-correlation that made the ℓ∞ _∞ bound vacuous — cuts the vocabulary sum to a few thousand head tokens at a stated price rather than for free: the tail-enveloped budget is 0.2760.276 at K=8192K=8192 against 0.04890.0489 over the full 129,280129,280-token vocabulary, a 5.6×5.6× envelope that degrades to 0.9670.967 at K=1024K=1024 and to a vacuous 1.2881.288 at K=64K=64. These belong to the per-layer bounded-difference route we retain as a diagnostic, and K=8192K=8192 is the smallest workable setting rather than headroom. Figure 5: The measurement that shaped the theorem. Per-layer propagation ratios ρℓ=‖Δh‖2/‖δ‖2 _ =\| h\|^2/\|δ\|^2 from random probes (4343 layers, noise floor exactly zero). A first-order response would make the two injection scales superpose; they separate by an order of magnitude at every layer, and the pre-registered linearity gate fails by a median factor of 14.114.1 (8686 layer–probe pairs, consistent with a saturated response: ρ∝ε−2ρ ^-2 gives 1616). We therefore do not report these as sound propagation constants; Theorem 1 is stated so no layer-local assumption enters it — the measurement rules out the cheap route to its constants, not the theorem. Removing the surrogate. Those draws were injected perturbations; the deployed rounding can be sampled directly, because the rounding seed mixes in the request identifier — repeating a prompt with radix caching disabled draws fresh rounding each time. Four pre-registered gates decide whether such a run means anything: compression must occur (1,999,5861,999,586 entries did), the draws must vary (all 160160 realized total variations distinct — coincidence would have meant re-running one draw, reported as failure), the arms must reconcile, and the bound must be non-vacuous. It is: ω[TV]≤ 0.0552vs.realized mean= 1.64×10−5,E_ω[TV]\;≤\;0.0552 . mean\;=\;1.64× 10^-5, (11) a factor of 3,3703,370 of slack, and the sample-size reading of that slack is controlled rather than inferred: an earlier pass of the same run at 5656 draws gave 0.14630.1463 with an essentially unchanged mean, so the constant tracks the sample and not the quantity. This is a statement about the deployed compressor rather than a stand-in for it. 6 The quantifier: extrapolating across histories Everything so far holds at a history. The theorem’s hypothesis is quantified over every history a request visits, and that gap is where the remaining distance to a deployed certificate lives. We measure it, and then close it on a stated population. One history is not enough — we measured how far from enough. We repeat the design across 8080 histories drawn without replacement from a pool of 148148 candidates (forty deployed-rounding draws each; 60,706,35760,706,357 compressed entries; the exact arm bitwise identical across repeats). The sampling design is not cosmetic: drawing without replacement from a stated pool makes the histories exchangeable by construction — exactly the hypothesis the extrapolation bound needs, and one our first attempt (histories enumerated at increasing lengths) did not satisfy. Figure 6 shows the outcome of the eighty-history design. Per-history mean total variation ranges from 2×10−62× 10^-6 to 2.6×10−12.6× 10^-1: a factor of 133,849133,849. The single-history number above sits at the insensitive extreme of that range and is not representative of anything. Figure 6: Eighty histories, one certificate each. (a) Realized mean served-output shift, sorted: five orders of magnitude separate the extremes, so the choice of history decides a single-history answer. (b) Certificates, each threshold against its own caliber: μcal _cal vs. Bonferroni-corrected upper bounds (∙ , α′=1.25×10−4α =1.25× 10^-4), μconf _conf vs. conformity scores (▲ , α=0.01α=0.01, no Bonferroni owed). Every held-out history clears both; held-out points never entered either threshold. The calibration procedure now certifies transfer. With a split fixed in advance (6464 calibration, 1616 held out), the certified reading is three-valued — a held-out history certifies when its upper bound falls below μcal _cal, is certified to violate only when its lower bound exceeds it, and is otherwise undetermined (comparing a noisy sample mean against a confidence bound decides nothing, which is how we first concluded otherwise). All 1616 held-out histories certify, and the result survives charging the draw-level confidence honestly: a Bonferroni split puts each history at α′=1.25×10−4α =1.25× 10^-4 and loosens μcal _cal to 0.51160.5116. Counting those outcomes gives a Clopper–Pearson bound of 0.25010.2501 on the rate at which a further history fails to certify — the weakest instrument available for the job (the full risk decomposition (26) and its sample-size arithmetic are in Appendix E); the conformal route below replaces it. The counting instrument was the bottleneck: a conformal replacement. That 0.25010.2501 is not what the data can support; it is what our instrument could extract. Counting held-out pass/fail discards the order structure among per-history scores — the only structure exchangeability needs. The order statistic uses it directly: for N+1N+1 exchangeable scores the events “score i is the strict maximum” are pairwise disjoint and equiprobable, so Pr(Snew>maxi≤NSi)≤1N+1, (S_new> _i≤ NS_i )\;≤\; 1N+1, (12) and a single union bound on top of (12) for the new history’s own coverage gives Pr(ω[TV∣hnew]>μconf)≤1/(N+1)+α (E_ω[TV h_new]> _conf)≤ 1/(N+1)+α (Lean: conformal_risk_union; disjointness is derived, exchangeability enters as an explicit hypothesis). On the identical 8080 histories this improves both numbers, but the two routes do not deliver the same kind of guarantee and we will not quote a ratio across kinds. The conformal 0.02540.0254 is a marginal bound: the probability is averaged over the calibration draw as well as the new history. The Clopper–Pearson 0.25010.2501 is a high-confidence statement about the calibration set we actually drew. Comparing them directly would repeat, one level up, the caliber swap this paper is about. The like-for-like comparison exists and we make it, matching the instrument to the sampling design: drawn without replacement from a finite pool, the textbook Beta(1,N)Beta(1,N) training-conditional bound does not apply (it assumes i.i.d. draws from a continuum), and the right object is the negative hypergeometric. With M=148M=148 pool members and N=64N=64 calibration draws, Pr(J≥j)=(M−jN)/(MN) (J≥ j)= M-jN/ MN for the number J of pool members exceeding the calibration maximum, so with probability ≥0.99≥ 0.99, J≤7J≤ 7, and a further draw misses coverage with probability at most 7/84=0.08337/84=0.0833 (0.09330.0933 with the new history’s own α added) — a 99%99\%-confidence statement of the same kind Clopper–Pearson makes, a factor of 2.72.7 against its 0.25010.2501, and the number we claim. (The marginal 0.02540.0254 is the right figure for long-run average risk across recalibrations, the wrong one for today’s calibration set.) The threshold itself tightens, from μcal=0.5116 _cal=0.5116 to μconf=0.4095 _conf=0.4095: calibration scores are conformity scores, not certificates, so the per-history Bonferroni split disappears — a fifth of the histories had been spent on a held-out check, and the rest charged twice. Figure 7: Same measurements, two instruments. Counting held-out pass/fail yields a single point; the order statistic yields a frontier, and the counting point is dominated on both axes. Moving along the frontier trades a looser certified budget for a smaller failure probability at no extra measurement. Exchangeable by construction, this is a bound on a stated population — the uniform distribution over the 148148-candidate pool — and we test it rather than assert it: the 1616 held-out histories are further draws from the same scheme, none exceeds μconf _conf (expected ≤0.25≤ 0.25 exceedances; the threshold never saw them). Figure 7 puts the two instruments in one plane: the paper’s recurring diagnosis turned on its own analysis, and the one instance where it buys a claim rather than killing one. What the bound does not cover is runtime traffic. The pool is built, and built narrowly (148148 truncations of a few base texts — prefixes, not the history stream a request walks), and 1616 test points against 0.250.25 expected exceedances make the held-out check a sanity check, not a powered confirmation. Closing that gap needs exchangeable sampling from real traffic, not a sharper inequality. What the order statistic changes is the cost of eventually getting there: at the marginal caliber a 1%1\% history sub-budget needs N=199N=199 exchangeably sampled histories (uneven splits are cheaper still), 2.32.3–5.3×5.3× fewer than the zero-event Clopper–Pearson route at the same total; the accounting, the request-level budget constraint (27), and Figure 8 are in Appendix G. What the experiment establishes is a certified cross-history bound on a stated population, premise met by construction and checked on held-out draws; what it does not establish is that the population is the one a deployed system faces, or that a runtime membership test and fallback exist. And the run fixes a prompt and a prefill-final position, varying only the rounding, so “anytime-valid” here means valid as draws accumulate — not along the histories an autoregressive request visits, which is what the theorem quantifies over. Lifting to runtime histories is the remaining structural step (a held-out design over domains, lengths and decode positions, a per-bucket bound, a fallback on leaving the calibrated set); the risk then reads as in (26), of which this paper accounts for the first two terms. Independence of draws across requests is assumed throughout. What supplies hypothesis (i). Two routes, same constant. Tensorization needs each layer’s contribution to depend on its own draw alone — the idealization our propagation probe falsifies. A Doob decomposition needs only bounded differences and carries the bias explicitly, [eF]≤exp([F]+∑ℓcℓ2/8)E[e^F]≤ (E[F]+ _ c_ ^2/8) (doob_mgf_le_biased), no layer-local assumption; joined to the composition’s shape by condE_eq_prod_sum and doob_mgf_prod_sum, the whole path is one theorem whose inputs are statements about the model and whose output is the request-level tail bound (request_tail_of_served_tv_doob_massweighted; one #print axioms returns the three standard axioms and nothing else). What remains is not a proof step but an instantiation: the constants cℓc_ in served-logit units from what the witness records — and our propagation measurement rules out the first-order surrogate. That is the open problem, and we state it as the paper’s main one. The cumulative tier, measured and soundly bounded. Running the armed model twice on eight fixed prompts — exact KV vs. deployed compression — and diffing the final next-token logits (Eout=‖Δlogit‖∞E_out=\| \|_∞ on the captured pre-head hidden state), the realized whole-request served TV is small: median 0.1180.118, worst 0.220.22 (Figure 4) — the cumulative served effect, end-to-end, non-vacuous. What sound bound certifies it? The obvious tanh(Eout) (E_out) is vacuous (0.9960.996): EoutE_out is a worst-coordinate quantity (median 3.13.1, sitting on a low-probability token), and total variation cares about mass movement, not the worst coordinate. The Bhattacharyya coefficient BC=∑vpvpv′BC= _v p_vp _v gives, by Cauchy–Schwarz on p±p′ p± p , the machine-checked bound TV(p,p′)≤1−BC(p,p′)2,BC(p,p′)=∑vpvpv′TV(p,p )\;≤\; 1-BC(p,p )^2, (p,p )= _v p_v\,p _v (13) (tv_le_hellinger) — and this sound bound is non-vacuous: median 0.160.16, worst 0.280.28, zero violations, within 1.4×1.4× of the measurement. So the cumulative served TV is not only measured small but bounded by a machine-checked sound certificate that breaks the ℓ∞ _∞ wall. A second machine-checked bound settles which regime the perturbation lives in. Reading the sub-Gaussian proxy off the realized perturbation (σ2=2lnp[eδ~]σ^2=2 _p[e δ], the tightest the measured MGF admits), served_tv_le_subgaussian certifies TV≤σ/2TV≤σ/ 2, evaluating to 0.230.23 (median, zero violations, within 2 2 of Hellinger — the price of variance alone). The decisive ratio σ2/Varp(δ)σ^2/Var_p(δ) has per-request median 0.990.99 (range 0.780.78–1.471.47): the realized perturbation is variance-tight — sub-Gaussian, not range-dominated — despite EoutE_out reaching 3.13.1–4.34.3 on the served position (18.918.9 at the worst prefill position). The large logits sit on low-probability tokens, so under p the MGF is governed by the variance (Varp(δ)≈0.115Var_p(δ)≈ 0.115), not the range — “mass movement, not worst coordinate,” read off the served softmax itself, falsifying the reading that a draw’s vocabulary spread must behave as a range. That measurement reshapes the a-priori target rather than closing it. The a-priori bound — from the witness budget alone, with no exact reference run — has its kernel machine-checked: a p-centred, ω-sub-Gaussian perturbation with proxy s2s^2 is within TV≤s/2TV≤ s/ 2 (served_tv_le_subgaussian), a pure variance bound with no worst-case range. Supplying that proxy from the witness involves two distinct randomnesses — the kernel’s is a vocabulary-softmax moment, the martingale’s is over rounding draws ω — so the guarantee is inherently one about ωE_ω, which is exactly the epistemics of the witness e-process. With the vocabulary moment measured variance-tight, what the proxy needs is a variance-scale bound on Varp(δ)=Δh⊤Covp(head)Δh≤trCovp(head)‖Δh‖2Var_p(δ)= h Cov_p(head) h \,Cov_p(head)\| h\|^2 (var_p_delta_le_trace_cov), with ‖Δh‖2\| h\|^2 carried back by the residual stream: writing Δh=∑ℓXℓ h= _ X_ , the increments are uncorrelated over ω, so ω‖Δh‖2=∑ℓω‖Xℓ‖2E_ω\| h\|^2= _ E_ω\|X_ \|^2 (14) — by (14) variances add, they do not accumulate as magnitudes (residual_second_moment_le) — which is why a witness that sums per-layer variances is the right budget. The uncorrelatedness is not assumed: modelling the draws as a product measure discharges it by Fubini (crossSum_indep_meanzero_eq_zero), and the per-layer propagation coefficients are bounded by a Frobenius envelope whose input norm the score bridge ties back to the witness (linear_propagation_frobenius, score_perturbation_l2_le). The CℓC_ here is the variance after propagation to the logits; relating it to the KV-side witness is the propagation constant we take up next. We measured those propagation constants on the armed model, and the measurement returned a negative result worth reporting. Injecting a random perturbation at each layer’s attention output and reading the served-position hidden state gives ρℓ=‖Δh‖2/‖δ‖2 _ =\| h\|^2/\|δ\|^2 with layer median 4.07×10−34.07× 10^-3 (range 7.2×10−57.2× 10^-5 to 4.9×10−24.9× 10^-2 over all 4343 layers, two probe directions each, zero-valued noise floor — repeated identical requests are bitwise deterministic), which by the Hutchinson identity puts ‖Jℓ‖F2\|J \|_F^2 near 5.6×1035.6× 10^3. But the pre-registered linearity gate fails: doubling-and-doubling the injection (ε ratio 44, hence energy ratio 1616) leaves ‖Δh‖2\| h\|^2 essentially unchanged, so ρ drops by a median factor of 14.114.1 instead of staying flat. A response that is independent of the injected energy is saturated, not linear. Empirically, then, the first-order surrogate Xℓ=JℓδaℓX_ =J δ a does not hold for this MoE at the perturbation scales we can inject — most plausibly because expert selection is an argmax and flips discontinuously. We therefore do not report these γℓ _ as sound propagation constants; they are a diagnostic that falsifies the linearization, and they say the right repair is not a better Jacobian estimate but a decomposition that never assumes layer-local dependence in the first place — a Doob decomposition Dℓ=[F∣ℱℓ]−[F∣ℱℓ−1]D_ =E[F _ ]-E[F _ -1], whose conditional MGF bound tolerates the true nonlinear, adaptive dependence. We take that step in the two places it is cheap and load-bearing. First, the Doob form. Replacing the falsified layer-local hypothesis with a Doob decomposition costs nothing in the constant: with Dℓ=[F∣ℱℓ]−[F∣ℱℓ−1],D_ \;=\;E[F _ ]-E[F _ -1], (15) and assuming only bounded differences — changing the ℓ -th draw moves F by at most cℓc_ — the same conditional-MGF machinery gives [eF]≤exp([F]+s22),s2=∑ℓcℓ24,E [e^F ]\;≤\; (E[F]+ s^22 ), s^2= _ c_ ^24, (16) — the bias carried explicitly, because stochastic rounding being unbiased per layer does not make the final logit unbiased once routing flips and activations intervene — identical proxy shape and constant, but now F may depend on the whole draw sequence nonlinearly and adaptively (doob_mgf_le). The modeling assumption, not the bound, is what weakens. Second, the bridge to a request-level budget. Our served-TV result is an expectation bound for one fixed output; a risk budget needs a tail bound over a request’s stream. The missing composition is short and we machine-check it: if a per-step loss satisfies 0≤Lt≤10≤ L_t≤ 1 with conditional expectation [Lt∣ℱt−1]≤μE[L_t _t-1]≤μ, then convexity of t↦eλt e^λ t on [0,1][0,1] gives the Bernoulli domination [eλLt∣ℱt−1]≤1+μ(eλ−1)E[e^λ L_t _t-1]≤ 1+μ(e^λ-1) (bernoulli_mgf_le) — an expectation-only hypothesis, no range bound needed beyond [0,1][0,1]. Taking ψ=log(1+μ(eλ−1))ψ= (1+μ(e^λ-1)) makes the e-process factor have mean at most one (eprocess_factor_le_one_of_expected), which is exactly the hypothesis our anytime ledger consumes, and composing yields Pr(∃t≤T:∑s≤tLs>Bt)≤δ (∃\,t≤ T:\ _s≤ tL_s>B_t )\;≤\;δ (17) (request_tail_of_expected_loss). So the beam (17) from expected loss to request-level tail is in place and machine-checked. Its left end is proved too, and by a modeling choice rather than new machinery: take the ledger’s event to be one decoding step’s entire vector of rounding draws. The one-step conditional expectation (2) requires is then literally the quantity our served-TV theorem bounds, evaluated at each history, so [Lt∣ℱt−1]≤μE[L_t _t-1]≤μ holds pointwise (request_tail_of_served_tv_massweighted). The ledger therefore closes on our theorem, not on a hypothesis. The name matters: the earlier request_tail_of_served_tv does carry a layer-local hypothesis — each layer’s contribution depends on its own draw — which our propagation probe falsifies; the mass-weighted form that Theorem 1 states carries none, its moment condition being written on the whole per-step draw vector. What remains open is instantiating its constants, not repairing its form. What is left is the model-specific numerics — the actual propagation constants ‖Jℓ‖F2\|J \|_F^2 and the first-order linearization Xℓ=JℓδaℓX_ =J δ a under which the increments are ω-local — not an intractable worst-case wall. Locating this precisely, machine-checking the entire propagation calculus (orthogonality discharged, Pythagorean identity, Frobenius envelope, score bridge, and the sound vocabulary-to-ω transfer), and measuring that the served perturbation lives on the tractable side of it, is what we contribute; instantiating the constants is open — and the measurement itself is single-step prefill, not a full multi-step decode. 7 From the witness to served output, per read A gate-parameterized served-TV law (per read). The physical gate admits a KV write only when its certified witness upper bound satisfies ue≤wthru_e≤ w_thr, and the audited realization never exceeds ueu_e, so every admitted read carries witness ≤wthr≤ w_thr by construction. Composing this gate fact with the Cauchy–Schwarz score bridge |Δscore|≤scale⋅‖q‖⋅‖Δk‖| | ·\|q\|·\| k\| and a tightened softmax bridge yields a closed-form ceiling on each admitted read’s attention TV. The softmax bridge is the crux: the inherited exponential-tilt form TV≤12(e2ε−1)TV≤ 12(e^2 -1) is vacuous at the perturbations at hand (ε≈0.70 ≈ 0.70 gives 1.541.54), but a moment/chord argument gives the machine-checked, uniformly tighter TV≤tanhεTV≤ (numerically the exact supremum is tanh(ε/2) ( /2), left as a conjecture). With it the per-read ceiling and its inverse become TV≤tanh(aqwthr),wthr⋆=atanh(τ⋆)/aq,aq=maxlayersscale⋅‖q‖,TV≤ \! (a_qw_thr ), w_thr =atanh(τ )/a_q, a_q= _layersscale·\|q\|, (18) — both machine-checked (served_tv_le_of_gate_tanh, gate_threshold_for_sla) — the first time the controller’s knob is tied to a served-output quantity by proof rather than by the empirical 0.9350.935. An ungated probe campaign supplies one self-consistent bridge measurement (aq=1.0034a_q=1.0034, sampled worst-key witness 0.700.70): reading 0.700.70 into the law gives tanh(0.70)=0.61 (0.70)=0.61 (0.340.34 under the tight conjecture), non-vacuous where the e-form gave 1.541.54 — but that is a sampling instantiation, the very substitution of a sample maximum for a gate constant this paper diagnoses elsewhere. The armed deployment’s actual threshold is wthr=35.34w_thr=35.34 (WITCERT_LEDGER_WTHR), where the same formula returns 1.0001.000: vacuous. We first recorded this as “the certified instantiation is open, pending an aqa_q measured on the armed model,” and that was the wrong diagnosis. The sound aqa_q needs no run at all. It is softmax_scale⋅‖q‖staticsoftmax\_ scale·\|q\|_static, where ‖q‖static=‖γ‖∞rmaxhσmax(Wq(b),h)\|q\|_static=\|γ\|_∞ r _h _ (W_q^(b),h) holds for every input and softmax_scale=d−1/2softmax\_ scale=d^-1/2 is a configuration constant, so it is same-model with the armed gate by construction. Evaluating it on the armed model gives aqsound=1.5067a_q^sound=1.5067 — only 1.50×1.50× the sampled 1.00341.0034. The bound was never the problem: wthr⋆=0.0332⏟needed for τ⋆=5%(sound)vs.wthr=35.34⏟deployed= 1064×, w_thr =0.0332_needed for τ =5\%\ (sound) . w_thr=35.34_deployed\;\;=\;\;1064×, (19) and of that 1064×1064×, the query envelope’s slack accounts for 1.50×1.50×. Tightening ‖q‖\|q\| — the open item we had named — cannot close a gap three orders of magnitude wide. One bound-side lever remains, and we charge it rather than let the previous sentence overstate the case. The Cauchy–Schwarz step behind aqa_q takes the worst point of a ball of radius W; replacing the ball by the measured error ellipsoid is the same move the companion paper makes for routing, where it bought 3.93.9–18.5×18.5×, and its ceiling here is the alignment factor d=512≈22.6 d= 512≈ 22.6. Charged on the armed model’s own captures, it buys nothing: 1.50×⏟‖q‖ bound⋅0.89×⏟ball→ellipsoid, measured⋅≈700×⏟gate operating point= 1064×. 1.50×_\|q\| bound\;·\; 0.89×_ball , measured\;·\; ≈ 700×_gate operating point\;=\;1064×. (20) The middle term is below one at the median and never usefully above it (0.390.39–1.131.13 across the 4343 layers) — the ellipsoid bound is looser than the ball it replaces — with zero violations on the held-out half, so this is not an artefact of overfitting the covariance. It is also not the trivial case of isotropic error: the stable rank of Cov(Δk)Cov( k) is 3737 of 448448, so the energy really is concentrated. What defeats the ellipsoid is its radius. The bound is r‖C1/2q‖r\|C^1/2q\|, and r is an extreme-value statistic in 448448 dimensions — it must cover the most outlying row along the low-variance directions, where C−1C^-1 is largest. Measured, r∈[25.5,31.1]r∈[25.5,31.1], above the isotropic reference 448=21.2 448=21.2: the radius gives back everything the anisotropy saves. On the routing side the same substitution replaces a per-expert ℓ∞ _∞ ball rather than an ℓ2 _2 one and pays off — a reminder that a technique’s payoff does not transfer across bound structures, and the reason we measured here rather than extrapolated. With all three layers now measured, “the residual is the operating point” is an observation rather than a conjecture. So the honest status is sharper than “instantiation is open”: the law is proved, its sound instantiation is in hand, and it says the deployed gate is nowhere near a per-read served SLA. Pillar A meets, in the per-read caliber, the same usability question that the companion paper settles for pillar B — with the difference that here the certified object is the right one, and only the operating point is wrong. The design law then reads a served SLA straight off the gate: certifying τ⋆=5%τ =5\% per-read TV needs wthr⋆≤0.05w_thr ≤ 0.05 in those witness units. The bound is not merely theoretical: reconstructing exact-versus-compressed attention on reads captured from the armed model (a synthetic pool — same-layer rank-0 reads merged without request identity, RoPE approximated), the machine-checked tanh bound holds on every sampled read/draw pair — zero violations, the tight tanh(ε/2) ( /2) included — while realized per-read served TV at the deployed 2-bit setting is small (median 0.030.03, worst 0.290.29). The inherited e-form is vacuous (≥1≥ 1) on 0.070.07 of these reads; tanh never is. Two honest limits remain: aqa_q here is a sampling maximum (the sound static envelope above is the backstop), and this measures the per-read attention tier — the cumulative final-logit perturbation is measured in §6 (served TV median 0.120.12, soundly bounded by 0.160.16). Proved Measured Open, declared per-step moment → request tail, (5)–(7); Doob form with no layer-local hypothesis; Bernoulli domination (8); conformal extrapolation (12) ω[TV]≤0.0552E_ω[TV]≤ 0.0552 on deployed rounding; 16/1616/16 held-out histories certify; 133,849×133,849× cross-history spread; +3.8%+3.8\% judgment cost propagation constants (probe falsifies the first-order surrogate); aqa_q and wthrw_thr from one gated run; population == our pool, not runtime traffic Table 4: What this paper does and does not claim. The middle column is evidence, not proof; the right column is what a deployed certificate still needs. Keeping these three apart is the discipline the paper argues for, and four of our own retractions came from letting them blur. Status of the claim. Table 4 summarises it. Established: the machine-checked kernel; the admission mechanism live in shadow, where the model-validation e-process leaves the radius model unrefuted over long real streams (706,909706,909 factors across eight 1,024-step decodes; peak logM=−3.70 M=-3.70 against a crossing threshold of 4.614.61) — that, and only that, is what the shadow numbers certify; the cumulative-loss theorem; the dual-accounting replay; and the physical-gate armed run (anytime ledger never crossed, budget dose-response, +3.8%+3.8\% overhead) with its held-out confirmatory replication (frozen λ and budget, topic-disjoint prompts, coverage gain same-round 0.140.14 vs. 0.300.30), which promotes the working point from exploratory to confirmed. Open and declared: pricing the physical witness account in served-output units. Per read that is now the machine-checked tanh law; cumulatively the additivity obstacle is dissolved — the residual stream makes the output-logit perturbation additive, so the whole request’s served TV is one tanh over a sum of per-layer bounds, TVrequest≤tanh(∑ℓbℓ)(cumulative_output_tv),TV_request\;≤\; ( _ b_ ) ( cumulative\_ output\_ tv), (21) rather than a product of per-layer factors — which is what made the aggregate tier reachable at all. What remains open at both tiers is a sound supremum for the query/Jacobian envelope (the aqa_q and bℓb_ factors), today measured rather than bounded — and, for the Jacobian factor specifically, our own measurement falsifies the first-order surrogate it would quantify (§5), which is why the Doob/bounded-difference form is the route we take — together with the graphs-on production fast-path overhead and the MoE expert-weight action. Until those land, pillar A is a proved engine with a validated substrate and a live physical controller — not yet a served-output guarantee a user can price. 8 Consequences for practice The first instruction has a five-arm replication on the serving stack itself. Running the RULER-style needle suite over five arms — an FP8 safe endpoint, a fully aggressive no-gate endpoint, and three gated configurations sharing one write threshold — with three independent server restarts per arm, every arm scores 1.0001.000 under the provably-clean caliber (zero evictions and zero ring-page recycling, both directly counted, which jointly rule out cross-request slot reuse) and zero authorization violations (Table 5). Quality does not separate the arms; the risk ledger does. The union-budgeted gate burns 99.4%99.4\% of its request budget on every twelve-document batch and pays a 59.3%59.3\% write-side fallback rate; the cumulative-loss gate at the same threshold holds a bounded account — peak charge 99.97%99.97\% of budget, with 4545 of 160160 admission calls budget-forced to exact — while paying only 56.3%56.3\%: the account that survives adaptivity also buys 33 points more coverage at equal quality. A shadow-audit arm reconciles the packed store against FP8 entry-by-entry (6.6%6.6\% mean relative residual), pricing what the compressed bytes actually hold. Arm acc clean risk ledger fallback FP8 safe (endpoint) 1.0001.000 ✓ none (no compression) — aggressive, no gate (endpoint) 1.0001.000 ✓ none — gated, union budget 1.0001.000 ✓ exhausts (99.4%99.4\% burned) 59.3%59.3\% gated, cumulative (phys) 1.0001.000 ✓ bounded (99.97%99.97\% peak) 56.3%56.3\% gated + shadow audit 1.0001.000 ✓ as union + reconciliation 57.5%57.5\% Table 5: Five-arm equal-quality table on the serving stack (DeepSeek-V4-Flash, tp8, three independent restarts per arm, medians; zero authorization violations anywhere). Caliber: the two endpoints bound the axis and are not co-axial with the gated arms; the gate acts on the write-side mantissa-mask layer while the packed compression itself runs identically in all four compressed arms; quality is stated only under the provably-clean caliber (zero evictions and zero ring-page recycling, both directly counted); fallback is reported as a rate because absolute event counts vary with batch composition. Throughput is a different caliber (concurrent clients) and is deliberately not a column of this table — and we disclose why: under mixed concurrent workloads (a benchmark warm-up preceding evaluation) the prototype’s c4-tier sparse-read path exhibits a localized defect (deep-position retrieval degrades while stored content verifies intact against the reference pool), traced to unresolved key-space translations and under repair. The quality column here is measured without such preceding traffic and is unaffected. Two instructions survive to the practitioner from this paper’s own scope, each carried by a measurement. First, budget risk with the anytime-valid account, not the union bound: the union budget exhausts on every long request while the physically-accounted gate holds its bound at every admission call and, in the held-out confirmatory round, halves the exact-fallback rate (0.30→0.140.30→ 0.14) at matched risk — coverage is bought at a price the account states, not found for free. Second, spend capacity where the workload can convert it: the 3.73×3.73× KV capacity that precision decisions bank converts to 1.19×1.19× throughput only under session reuse, and to nothing under one-shot traffic (Table 8); the decision to buy is a workload property, not a systems constant. The routing-side prescriptions — what not to certify, what not to preserve, and where the freed budget should go — are collected with their measurements in the companion paper’s prescriptive table. 9 Related work Four properties would have to hold at once for a precision decision to be both trustworthy and deployable: it must be made per request, it must carry a sound statement rather than an average one, that statement must survive adaptive decoding (where earlier quantized state feeds later queries), and it must run inside a serving stack. Table 6 reads the literature against those four. The pattern is that they never co-occur — offline work buys soundness by giving up request conditioning, dynamic-precision serving buys request conditioning by giving up the guarantee, and the certified line that has both is confined to the KV domain and budgets by union bound. Per- Sound Adaptive- In serving Line of work request (not avg.) valid stack PTQ / second-order weighting ✗ ✓ — ✗ GPTQ, AWQ, QERA, YAQA, WaterSIC MoE quantization (expert/router-aware) ✗ ✗ — ✗ MoEQuant, GEMQ Dynamic-precision serving ✓ ✗ ✗ ✓ MorphServe, DP-LLM, QAQ Certified runtime quantization (KV) ✓ ✓ ✗ ✓ Calver, WitCert This paper (served-output budget) ✓ ✓ ✓ ✓ Table 6: Why the gap is structural rather than incremental. “Adaptive-valid” means the guarantee survives the feedback of quantized state into later queries — a union budget over a pre-declared event count does not, which is the deficit §4 removes. “—” marks lines that make no per-step claim, so adaptivity does not arise. The routing column is absent by design: no prior line certifies routing, and §3 is our evidence that certifying it would not have helped. Certified runtime quantization (KV domain). Runtime certificates with fallback exist for quantized attention [1] and for KV-cache quantization with request budgets and Lean-checked kernels [15]; these establish request-conditioned sound bounds in serving loops. The former’s guarantees are deterministic only under stated preconditions, are self-described as infeasible for batched serving, and — by its own limitations section — its per-step bounds “do not compose into an end-to-end budget”; the latter budgets by union bound. Neither touches routing, and neither survives adaptive decoding with a valid request-level budget — the two deficits this paper addresses. PTQ with activation/second-order weighting. GPTQ/AWQ-style calibration [4, 10], closed-form error reconstruction [16], KL-Hessian rounding [13], and information-theoretic allocation with provable rate gaps [9] sharpen offline average objectives; none yields a per-instance serve-time certificate, a distinction WaterSIC’s own limitations section is candid about. Dynamic-precision serving. MorphServe [12] swaps quantized layers on load signals; DP-LLM [7] selects per-step precision by empirical thresholds; query-adaptive QAQ [8] uses a trainable router over bit-planes. Request conditioning and serving integration appear — but guarantees do not, and the two properties never co-occur. MoE quantization. Expert-balanced calibration [6], global expert-level bit allocation with router fine-tuning [3], routing-consistency calibration losses [11, 5, 2], and routing-consistency-regularized binarization (MoBiE [17], withdrawn by its authors in April 2026): all offline; GEMQ’s measured 41.31%41.31\% expert-selection shift at 1.5-bit demonstrates the fragility, none provides an online guarantee. Production MXFP4 DeepSeek checkpoints quantize expert projections only and exclude the router — consistent with our gate-arm measurement. The routing-replay and equal-byte comparisons that adjudicate what these methods protect are the companion paper’s subject; here they enter only through the boundary §3 states. Anytime-valid inference. E-processes and confidence sequences are mature for answer-quality monitoring of LLMs; what they buy over a union budget is Ville’s inequality, Pr(∃t≥0:Wt≥1/δ)≤δ (∃ t≥ 0:W_t≥ 1/δ)≤δ for a nonnegative supermartingale wealth process with W0=1W_0=1 — the quantifier inside the probability, no horizon declared, survival under adaptive stopping. To our knowledge no prior work drives quantization precision decisions from such a budget; §4 is where we do, and also where we show that wealth alone is not a per-action risk account. 10 Limitations Four limits bound what this paper claims, and we state them at the level that changes a reader’s conclusion; the full enumeration, gate by gate, is Appendix H. Choosing the certified predicate is outside the machinery, and choosing it wrong is invisible from inside. §3 is a worked instance: the routing certificate issues, its soundness is a theorem, its violation count is zero on nine models and 485,138485,138 tokens, and every internal indicator is green — while the product is vacuous, because the predicate it establishes does not bound the quantity anyone cares about (the routing-TV split identity (companion paper)). No amount of tightening, and no check the framework can run on itself, would have revealed that; only stepping outside and asking whether P implies the served effect does. We report this as the most transferable finding in the paper and as a standing limitation of the approach, not as an anecdote about one bad predicate. The population is ours. The conformal bound holds on a 148148-candidate pool we constructed, not on runtime traffic and not along the history stream an autoregressive request actually walks: Prpool(Snew>q^)≤0.0933⏟proved, M=148 constructed histories⟹̸Prtraffic(Snew>q^)≤0.0933⏟what deployment needs. _pool (S_new> q )≤ 0.0933_proved, M=148 constructed histories\;\; \;\; _traffic (S_new> q )≤ 0.0933_what deployment needs. (22) Closing the gap needs exchangeable sampling from real traffic, not a sharper inequality. The constants are measured, not bounded. Propagation constants, the query envelope aqa_q, and the gate threshold wthrw_thr are each measured on one run or one model; our own probe falsifies the first-order surrogate a tensorized proof would need, which is why Theorem 1 is stated for an arbitrary step perturbation. The witness is local. The physical account charges a band-norm of the K/V residual, not served total variation; the bridge between them is proved per read and open in the aggregate. 11 Conclusion Certified precision for MoE serving must first certify the right object — and getting that wrong costs a misdirected budget, not a loose bound (§8). The companion paper’s adjudication shows it is not routing invariance — flips are pervasive and benign — and a counterexample we aimed at our own first design shows it is not e-process wealth dressed up as per-action risk. What remains standing is precise, and we prove it: quantization damage is a cumulative tail phenomenon of the served output, and a per-step mass-weighted exponential-moment budget bounds it — a per-vocabulary bias-and-fluctuation bound weighted by served probability, stated in served-logit units, with the map from the KV-local witness still open. Theorem 1 carries that budget to a mass-weighted expected served-output total variation and then, through a domination that needs only that expectation, to a request-level tail bound: [TVserved]≤B⏟mass-weighted expectation⟹Pr(TVserved≥τ)≤B/τ⏟request-level tail. E [TV_served ]≤ B_mass-weighted expectation\; \; (TV_served≥τ )≤ B/τ_request-level tail. (23) The composition is machine-checked, and — after our own propagation probe falsified the layer-local idealization — it is stated so that no such idealization enters it. The moment hypothesis it consumes is itself proved from bounded differences alone, with the bias carried explicitly, and the two are joined by a proved equality of the conditional-expectation and product-measure forms. What is left open is not a proof but an instantiation: supplying the bounded-difference constants for a real network, in served-logit units, from what the KV-side witness records. That is the paper’s methodological point as much as its technical one — the experiment that failed dictated the shape of the theorem that stands. The measured components are cheap (audit witnesses the write path already produces); the controller’s own serving judgment costs +3.8%+3.8\% wall time (measured); what is not yet measured is the graphs-on production fast path. The soundness is machine-checked where it is probabilistic, and every gate that shaped the system — including the negatives that killed our own designs — is pre-registered and artifact-traceable. Appendix A Per-gate experimental record All gates were pre-registered: verdict branches were committed to the repository before the corresponding data existed, and every number below is frozen in a machine-generated canon that traces to a run artifact. Captures carry provenance stamps (machine, code hash, tree digest) and declare their accounting keys; a conformance guard rejects products whose declared keys are degenerate (a failure mode we hit and formalized during this campaign). Activation geometry (gate W2-a). Table 9 summarizes per-stream spectra. Both models pass the pre-registered concentration bar on attention streams; the MoE passes on all three. Held-out energy is computed by fitting the top-7.1%7.1\% eigenspace on even-parity requests and evaluating on odd-parity requests (flat-spectrum baseline 0.0710.071). KV-side honesty (gates K0, K0′, K0-R). The pre-registered kill-shots that redirected this paper: on synthetic pools the certified-vacuous stratum was empty (43/43 layers non-vacuous even at 4-bit masking) and no condemned read was rescuable (rank correlation 0.8720.872 between realized distribution shift and realized output error); the real-pool recheck is a stronger negative rather than a confirmation: across 189189 same-request pools (depth ≥64≥ 64, request-matched queries, RoPE segment included) the INT6/4/3 family never produces a distribution shift above the condemnation bar, so the condemnation stratum is empty (00 points) and that run’s own pre-registered branch is “inconclusive, no high shift” — there is nothing to rescue in the deployed regime because nothing gets condemned. The shift-to-error rank correlation there is 0.9350.935. The two pools fail the rescue hypothesis in different ways, which is why the second is the stronger result: 1,528condemned, 0rescued⏟synthetic pool: rescue exists to test, and fails0condemned⏟real pool (189): nothing to rescue. 1,528\ condemned,\ 0\ rescued_synthetic pool: rescue exists to test, and fails 0\ condemned_real pool ($189$): nothing to rescue. (24) The query-side spectrum pilot (ρ90=0.094 _90=0.094 in-sample against 0.5380.538 held-out energy at n≪dn d, verdict gray) is retained as the small-sample cautionary control that shaped the W2-a design. GLM-5.2, identical hardware FP8 W4AFP8 ratio Aggregate throughput, C=128C=128 (tok/s) 1,7891,789 1,8341,834 1.03×1.03× Aggregate throughput, C=512C=512 (tok/s) 1,8271,827 1,8691,869 1.02×1.02× KV-cache capacity (resident tokens) 291,968291,968 1,087,8081,087,808 3.7×3.7× Errors, full 1..1281..128 sweep 00 00 — Table 7: Throughput is flat to within single-run spread at both concurrencies — we report the spread rather than claim equivalence, since no restart confidence intervals were collected — while configured resident-token headroom grows 3.7×3.7×. On this short-context workload neither arm reaches its KV wall. Table 8 pressure-probes the headroom and reports what it does and does not convert to. The capacity figure here is configuration-derived, not an OOM limit. no prefix reuse session reuse 2626k-token requests, GLM-5.2, W4AFP8 vs FP8 (worst case) (agent-shaped) Configured KV capacity 3.73×3.73× → concurrent requests 2.0×2.0× 2.24×2.24× → warm-prefix hits — (none) 1.93×1.93× → throughput 0.960.96–1.01×1.01× 1.071.07–1.27×1.27× → TTFT (p50) — 1.081.08–1.20×1.20× (0.92×0.92× at C=256C=256) Table 8: What 3.7×3.7× of KV capacity converts to, pressure-probed in two workloads. Left: every request is a fresh slice of text, so the prefix cache never hits (peak cached tokens 2,5602,560 and 00 against a 26,00026,000-token prompt). FP8 runs at 100%100\% pool occupancy and W4AFP8 at 58%58\%, so the capacity does buy 2×2× the in-flight requests — and buys nothing in throughput, because at this prompt length the work is prefill-bound and the GPU is already saturated. Right: each session keeps its own long context and reuses it across turns, the shape a coding agent has. Now capacity decides how many sessions stay cache-warm: FP8 is pinned at 1010–1111 resident sessions per rank (its pool holds 291,968/26,500=11.0291,968/26,500=11.0) at 100%100\% occupancy, while W4AFP8 holds 2323–2424 at 54%54\%. Every link in the chain attenuates, and the last one attenuates hardest — what a hit saves is prefill, while steady-state throughput is still set by decode and compute. Two caveats we state rather than bury: the TTFT gain reverses at C=256C=256, where W4AFP8’s larger running batch leaves each request less compute, so the throughput is bought with per-request latency; and each session completes only ≈1.9≈ 1.9 turns inside the measurement window, so 1.19×1.19× is a lower bound on what a real multi-turn session would show — we do not extrapolate it. Protocol: per-level prefix namespaces and a 9090 s warm-up per level; without both, prefixes carry across levels and the measurement reports a spurious 1.58×1.58×. Capacity–cost evaluation (gate W3, measured). On GLM-5.2 served with the production stack (tp8/ep8/dp8, FP8 KV cache, CUDA graphs, radix on; both arms at matched memory fraction 0.850.85 after a pre-registered arm death at 0.880.88 taught us the W4AFP8 runtime workspace requirement), the W4AFP8 checkpoint is throughput-neutral at matched concurrency — 1,8341,834 vs 1,7891,789 aggregate tok/s at C=128C=128, with TTFT/TPOT curves overlapping within single-run spread and zero errors across the full 1..1281..128 sweep on both arms (we report the spread rather than claim statistical equivalence, since no restart confidence intervals were collected) — while its server-reported KV-cache capacity is 1,087,8081,087,808 vs 291,968291,968 tokens (Table 7): 3.7×3.7× the configured resident-token headroom on identical hardware (a configuration-derived figure, not a pressure-probed OOM limit; throughput parity is from single runs without restart confidence intervals). An extended sweep to C=512C=512 sharpens the interpretation: both arms hold a compute-saturation plateau (1,8691,869 vs 1,8271,827 tok/s at C=512C=512) with zero errors and matching queueing growth — on this short-context workload neither arm reaches its KV wall, so the capacity headroom is banked, not spent; it becomes serving value exactly where resident tokens bind (long contexts, large batch memory), which is the production regime the deployment reports describe. Every level of both arms passes a machine adjudicator (per-level liveness, matched level sets, capacity fields on record) whose falsifiability is enforced by a real negative fixture: the run in which one arm died mid-sweep and six dead windows masqueraded as measurements. Appendix B Request-conditioned activation geometry (precondition test) Both pillars consume a bound on how quantization error in a weight W projects onto the activations x the current request actually produces: for error E=W−W^E=W- W, the served perturbation is ExEx, and ‖Ex‖2=tr(EΣxE⊤)E\|Ex\|^2=tr(E\, _x\,E ) for Σx=[xx⊤] _x=E[x ]. The decision-relevant question is whether Σx _x has usable low-dimensional structure, and whether the structure measured on one phase of a request predicts the other. Measurement. We accumulate exact second moments Σ=X⊤X =X X per (layer, stream, phase, request-parity) on the three activation streams every transformer block exposes (attention input, attention-output projection input, MLP/MoE input), on 16 teacher-forced requests (16 requests, 2048/4096-token prefills plus 128 forced decode steps; 3×1043× 10^4-row order per stream, n≫dn d). Split-half (request-parity) held-out energy and prefill→ transfer are controls against the small-sample bias that a pilot study on the KV query side taught us to fear: at n=96≪d=448n=96 d=448 the in-sample spectrum looked concentrated (ρ90=0.094 _90=0.094 of eigendirections) while held-out energy at the matched rank reached only 0.5380.538 — above the flat-spectrum baseline but below the pre-registered 0.700.70 bar, a gray verdict rather than a collapse. At n≫dn d the gap closes. Model Stream ρ90 _90 Held-out Verdict Qwen2.5-7B attn-in 0.0340.034 0.8290.829 concentrated Qwen2.5-7B o-proj-in 0.03320.0332 0.7420.742 concentrated Qwen2.5-7B mlp-in 0.04440.0444 0.6600.660 gray DeepSeek-V2-Lite attn-in 0.00440.0044 0.9460.946 concentrated DeepSeek-V2-Lite o-proj-in 0.02640.0264 0.8440.844 concentrated DeepSeek-V2-Lite moe-in 0.04440.0444 0.7920.792 concentrated Table 9: Gate W2-a: activation second-moment spectra with held-out validation. ρ90 _90 = fraction of eigendirections carrying 90%90\% of energy (prefill, per-layer median). Findings (pre-registered thresholds). On DeepSeek-V2-Lite all three streams pass the concentrated verdict: the top 0.440.44–4.4%4.4\% (ρ90 _90 per stream: 0.00440.0044, 0.02640.0264, 0.04440.0444) of eigendirections carry 90%90\% of energy, and a subspace fitted on even-parity requests captures 0.9460.946/0.8440.844/0.7920.792 of odd-parity energy at rank 7.1%7.1\% of d (flat-spectrum baseline: 7.1%7.1\%). On Qwen2.5-7B the attention streams pass (ρ90 _90 0.0340.034/0.03320.0332, held-out 0.8290.829/0.7420.742); the MLP stream falls in a pre-registered gray zone (held-out 0.6600.660 against a 0.700.70 bar, ρ90 _90 0.04440.0444). Crucially, coordinate-basis (diagonal) concentration is far weaker (an order of magnitude more coordinates for the same energy): the structure is off-diagonal, so per-channel scaling — the diagonal special case — cannot exploit it. This replicates, on the weight side, a negative prior we measured for diagonal query-weighting in KV quantization. Arm Hypothesis under test Verdict Key number Gate quantization router survives INT4 killed 63.2%63.2\% flips Upstream margins exact gate suffices killed 93.7%93.7\% binding Flip→ flips predict damage dissociated R 0.710.71–0.840.84 Natural text damage is average-case killed Δ 0.00020.0002 Value-transport condemned reads rescuable killed 00/1,5281,528 Served-output tail the object that survives adopted TV 0.1180.118/bd. 0.1590.159 Propagation probe first-order surrogate holds killed linearity 14.114.1 Bounded differences budget is non-vacuous model-dep. 0.04890.0489 (diagnostic) Layer-local plug-in product of per-layer moments model-dep. 0.03900.0390 (diagnostic) Joint scalar moment the functional the theorem needs supported pt. est. 0.00230.0023 Betting confidence seq. bound free of sample extrema supported [TV]≤0.0322E[TV]≤ 0.0322 Deployed rounding the surrogate is removable supported [TV]≤0.0552E[TV]≤ 0.0552 Cross-history spread one history represents all killed 133,849×133,849× Cross-history certif. calibrated bound transfers supported 16/1616/16, ≤0.0254≤ 0.0254 Lipschitz envelope sound cℓc_ from weights killed 1022110^221 Local envelope contractive as a supremum killed σmax≈16 _ ≈ 16 Table 10: Every design hypothesis we tested, including the ones aimed at our own proposals. The companion paper’s five pre-registered arms eliminate routing invariance as the certified object; the served-output tail is what survives, and is what Theorem 1 bounds. The last row is the measurement that falsified the first-order propagation surrogate and thereby fixed the form of the theorem. Numbers are the same artifacts cited in the text. Appendix C Proof sketch of Theorem 1 (machine-checked chain) Proof (machine-checked). Figure 1 shows where this theorem sits in the chain and what it does not reach. The statement above is request_tail_of_served_tv_massweighted; its Doob-supplied form, taking bounded differences directly as input, is the single root theorem request_tail_of_served_tv_doob_massweighted. Per draw, the sub-Gaussian kernel gives TV≤logZ(ω)TV≤ Z(ω) via BC≥e−σ2/4BC≥ e^-σ^2/4 and TV≤1−BC2TV≤ 1-BC^2; concave Jensen for ⋅ · then log , and a Fubini step giving ωZ=∑vph(v)ω[eδh(⋅,v)]E_ωZ= _vp_h(v)E_ω[e _h(·,v)], yield the mass-weighted step bound — note the weighting by ph(v)p_h(v) is what keeps a large perturbation on a low-probability token from dominating, and it is why the bias bh(v)b_h(v) can be priced rather than assumed away. Convexity of t↦eλt e^λ t on [0,1][0,1] then gives the Bernoulli domination [eλTV]≤ 1+μ(eλ−1),E [e ]\;≤\;1+μ (e^λ-1 ), (25) whose mean-one e-process factor — the right-hand side of (25) — is exactly what the anytime ledger consumes; taking one decoding step’s whole draw vector as the ledger’s event makes hypothesis (i) a conditional statement at every history, which is what the ledger needs. Axioms are the three standard ones, no sorry. Appendix D The step budget is of the right order: caliber Is the budget of the right order? The theorem is only useful if the quantity it consumes, log∑vph(v)Bh(v) _vp_h(v)B_h(v), is far below 11 at a real operating point. We can bound the shape of that quantity without a new experiment, and we have to be exact about what that does and does not show. Substituting one realized draw ω0 _0 for Bh(v)B_h(v) — i.e. computing log∑vph(v)eδh(ω0,v) _vp_h(v)e _h( _0,v) — gives 0.2300.230 (median over the 88 captured requests, 0.3970.397 at the maximum) against a realized served TV of 0.1180.118. This is a realization of the object, not a bound on it: hypothesis (i) asks for ω[eδ]E_ω[e^δ], and a moment generating function is precisely where a typical draw and its expectation part company — a rare large δ contributes nothing to ω0 _0 and everything to ωE_ω. So the honest reading is that the object the theorem prices is of the right order where the system runs, and that three things stand between that and a certificate: obtaining Bh(v)B_h(v) a priori from the witness rather than from a reference run; replacing the realized draw by a bound on its ω-expectation; and replacing a median over eight requests by a bound at every history, which hypothesis (i) quantifies over. The next section’s propagation measurement attacks the first; §A measures the third and finds it is where the real distance lies. Appendix E The binomial route and its risk account Counting those outcomes gives a Clopper–Pearson bound of 0.25010.2501 on the rate at which a further history fails to certify. That is a bound on the certification procedure rather than on the truth, and it is the weakest instrument available for the job; the next paragraph replaces it. A complete risk account reads δtotal=δledger+αdrawtotal+phistoryUCB+βhistory, _total\;=\; _ledger+ _draw^total+p_history^UCB+ _history, (26) the last term pricing the confidence in the history-failure-rate estimate itself. Reaching a 1%1\% history-failure rate at 99%99\% confidence with zero violations needs on the order of 459459 histories by this route; a hundred would reach roughly 4.5%4.5\%. Appendix F Adjudication notes for the dual-accounted admission table Three calibers govern how Table 2 may be read. Cross-run comparison. A separate offline dual-accounting run over 3636 request accounts puts the median upper bound on the union fallback rate at 31.0%31.0\%; different run, different population, and neither bounds the other. The coverage gain is also not like-for-like: the guaranteed object changes from a per-event family to a cumulative account, which the run’s own caliber note states. Physical-gate non-vacuity. The physically-accounted gate (WITCERT_CUMLOSS_MODE==phys) stays non-vacuous — the tail term is 0.67%0.67\% of the accumulated mean term, not of the budget — with the certified bound sitting 4.6%4.6\% above the realized witness at the request endpoint (median over 1616 endpoints). Judgment cost. The cost is not monotone in the budget: the tight arm runs 1.5%1.5\% faster than the union baseline while the open arm runs 3.8%3.8\% slower, so the +3.8%+3.8\% quoted elsewhere is that arm’s figure, not a property of the mechanism. Appendix G The history cost of the certificate Continuing from the marginal/conditional distinction of §6: What the order statistic changes is the cost of eventually getting there. Both terms must be priced together, since 1/(N+1)+α≥α1/(N+1)+α≥α. Splitting a 1%1\% history sub-budget evenly gives α=0.005α=0.005 and N=199N=199 histories at the marginal caliber; splitting it unevenly is cheaper still (α=0.001α=0.001 needs N=111N=111). A training-conditional statement at the same target needs more, and how much more depends on the population size. We stress that this is the history term of (26) alone. A request-level budget must satisfy δledger+αconf+1N+1≤δreq, _ledger+ _conf+ 1N+1\;≤\; _req, (27) so by (27) the sample size follows from δreq _req only after δledger _ledger is frozen; at our present configuration the two accounts together are 1%+2.54%1\%+2.54\%, not 1%1\%. Comparing against zero-event Clopper–Pearson at the same total is budget-dependent in the same way: 459459 histories if its 1%1\% is charged entirely to the bound value, 1,0571,057 if its confidence is charged separately as we charge ours. We quote the conservative end — 2.3×2.3× fewer histories — and note the honest range is 2.32.3 to 5.3×5.3×. Figure 8 traces the requirement across targets. Figure 8: What the instrument costs in histories, at the marginal caliber and in the large-population limit. Number of exchangeably sampled histories needed to certify a given bound on next-history failure, splitting the budget evenly between the two terms; the Clopper–Pearson curve is the zero-event requirement at 99%99\% confidence. A training-conditional guarantee costs more, and a finite pool costs more still — our own 8080-history run reaches 0.02540.0254 marginally but 0.09330.0933 conditionally. The two follow different scaling laws, so the gap widens as the target tightens — which is the long-run argument for the order statistic, independent of the factor we measure at 8080 histories (⋆ ). Appendix H Full limitations, gate by gate (i) The routing arms run on DeepSeek-V2-Lite, a 6464-expert model with greedy top-k selection. We have since re-measured on the serving-line model itself — DeepSeek-V4-Flash, 256256 experts top-66 under bias-corrected routing — and the verdict is unchanged and stronger (99.0%99.0\% binding at INT4 against 93.7%93.7\% on the proxy, zero soundness violations). That gap is now closed the rest of the way: the nine-model sweep of §3 includes GLM-5.2 (99.9%99.9\%), MiniMax-M2.7, Qwen3, gpt-oss, Kimi-K2.5, Mixtral and Llama-4-Scout, so the residual exposure is no longer which family but which selection rule: a two-stage (grouped) rule must charge both stages, and only the second is the familiar one, mgroup>4Lε∞⏟group stage (a sum of two perturbed scores)∧mexpert>2Lε∞⏟within-group stage. m_group>4L _∞_group stage (a sum of two perturbed scores) m_expert>2L _∞_within-group stage. (28) Rules we have not measured — learned or hashed assignment, or >2>2-stage selection — are not covered by (28) and remain open. (i) The upstream logit-error radius used online must itself be certified from activation geometry (Appendix B); the teacher-forced measurement in §3 bounds achievable behavior, not the deployed bound’s tightness. (i) Our first router-margin arm conflated perturbation sources (gate vs. upstream); we report both arms and the correction openly. (iv) The value-transport rescue hypothesis for KV quantization died its pre-registered death on synthetic pools (rank correlation between attention-distribution shift and realized output error 0.8720.872; zero rescuable reads among 1,528 condemned). The real-pool recheck is not a confirmation of the death but a stronger negative: under the production quantizer family no read even reaches the condemnation bar, so the condemnation stratum is empty (00 points) and that run’s own pre-registered verdict branch is “inconclusive, no high shift”; the rank correlation there is 0.9350.935. This paper claims nothing about output-visible rescue. (v) Cross-layer propagation of weight-error into router inputs is measured, not bounded; hidden-state bridges remain empirical tier. (vi) The armed controller’s current action is KV-write precision; expert-weight precision switching is motivated and priced here but not implemented. (vii) The witness-to-served bridge is closed as a theorem (Theorem 1) but not as a deployment: its per-layer budget CℓC_ is stated in served-logit units, whereas the runtime witness accounts in KV-local units, and the constant relating them is exactly what our propagation probe failed to certify (the response saturates, so the first-order surrogate that would supply it is invalid). Until that constant is bounded — not estimated — the theorem prices a budget the deployed ledger does not yet emit. (viii) The bounded-difference constants cℓc_ are now measured directly, and the budget they produce is non-vacuous (0.04890.0489, with the bias measured rather than assumed), but they are empirical maxima — lower bounds on the supremum a sound certificate needs. Closing this means a genuine envelope for the compressed path; the composition rule is proved (bdd_diff_of_lipschitz), but instantiating it from the deployed weights yields 1022110^221 and rules a global envelope out. The local route is formalized with its extra obligation explicit (bdd_diff_of_lipschitz_on, lip_iterComp_on); the ladder it buys is large and still not enough: 10221⏟global envelope⟶σmax≈16.0⏟local, along the trajectory⟶effective rank 42⏟what actually settles it, 10^221_global envelope\; \; _ ≈ 16.0_local, along the trajectory\; \; effective rank 42_what actually settles it, (29) a hundred-plus orders of magnitude for the first step, yet σmax>1 _ >1 is expansive, so a Hoeffding bound is still vacuous. Our own reading of the typical ratio (0.06380.0638) as a Lipschitz constant was wrong and we retract it. The repair the rank indicates is a Bernstein-type moment bound calibrated to it rather than a Hoeffding bound calibrated to a supremum. Deriving and machine-checking that bound is the concrete next step, together with verifying forward invariance online. (ix) Our per-layer plug-in numbers (0.03900.0390, 0.04890.0489) are diagnostics under the layer-local additive model, not instantiated budgets: multiplying single-layer moments assumes exactly the additivity the saturation measurement rejects. One interface mismatch remains in the same direction — the measured quantity is a maximum against a single baseline, not a diameter over pairs of draws (the other, a vocabulary-shared constant, we removed by indexing per token in the theorem). The experiment that removes both at once, a joint resample of every layer reduced to one scalar per draw, we report. An empirical Bernstein bound gives 0.20860.2086, but it takes its range R from the sample maximum rather than a deterministic bound, so it is a diagnostic, not sound. It mirrors the Bernstein row of Table 3: there the range was too large and the bound went vacuous; here it is too small and the bound stops being valid. The gap is closed properly instead: total variation is deterministically bounded in [0,1][0,1], so a betting-style confidence sequence certifies ω[TV]≤0.0322E_ω[TV]≤ 0.0322 with no appeal to a sample extremum. The proxy then goes too: repeating an identical prompt draws fresh deployed rounding each time, and on those real draws — compression verified to occur, every realized total variation distinct — the same sequence gives ω[TV]≤0.0552E_ω[TV]≤ 0.0552: ω[TV]≤0.0322⏟synthetic draws, no sample extremumω[TV]≤0.0552⏟deployed rounding, 160 distinct real draws. E_ω[TV]≤ 0.0322_synthetic draws, no sample extremum E_ω[TV]≤ 0.0552_deployed rounding, 160 distinct real draws. (30) What separates this paper from a deployed certificate is therefore neither the surrogate nor the inequality but the quantifier: the theorem asks its hypothesis at every history a request visits. We establish it at 8080 histories drawn exchangeably from a stated pool spanning 133,849×133,849× in sensitivity, and certify transfer to an unseen member with failure probability ≤0.0254≤ 0.0254; all 1616 held-out histories certify. Two distinctions carried that result, and neither is pedantry. Reading “did not certify” as “violated” is the same error, one level up, as reading a sample mean as a bound — we made both before catching them. And an unmet exchangeability premise turns a bound into an efficiency ceiling, not a risk account, which is why we rebuilt the history family as a without-replacement sample. The population is still ours, not runtime traffic; risk is reported as in (26). References [1] D. Calver (2026) Runtime-certified bounded-error quantized attention. arXiv:2605.20868. Cited by: §9. [2] Y. Chen, Y. Shao, P. Wang, and J. Cheng (2025) EAC-MoE: expert-selection aware compressor for mixture-of-experts large language models. In ACL, Note: arXiv:2508.01625 Cited by: §9. [3] J. Deng, S. Wang, D. Wang, Z. Liu, T. Chen, H. Yang, and J. Hu (2026) GEMQ: global expert-level mixed-precision quantization for MoE LLMs. In ICML, Note: arXiv:2605.23078 Cited by: §1, §9. [4] E. Frantar, S. Ashkboos, T. Hoefler, and D. Alistarh (2023) GPTQ: accurate post-training quantization for generative pre-trained transformers. In ICLR, Note: arXiv:2210.17323 Cited by: §9. [5] Z. Fu, T. Zhao, N. Ding, X. Yu, X. Li, Y. Tang, and Y. Wang (2025) EAQuant: enhancing post-training quantization for MoE models via expert-aware optimization. arXiv:2506.13329. Cited by: §9. [6] X. Hu, Z. Chen, D. Yang, Z. Xu, C. Xu, Z. Yuan, S. Zhou, and J. Yu (2025) MoEQuant: enhancing quantization for mixture-of-experts large language models via expert-balanced sampling and affinity guidance. arXiv:2505.03804. Cited by: §9. [7] S. Kwon, S. H. Seo, J. W. Lee, and Y. Park (2025) DP-LLM: runtime model adaptation with dynamic layer-wise precision assignment. In NeurIPS, Note: arXiv:2508.06041 Cited by: §9. [8] S. Li, H. Liu, Z. Wang, R. Du, S. Lee, C. Tian, and Q. Li (2025) QAQ: query-adaptive mixed-precision quantization for large language models. In NeurIPS Workshop on ML for Systems, Cited by: §9. [9] E. Lifar, S. Savkin, O. Ordentlich, and Y. Polyanskiy (2026) WaterSIC: information-theoretically (near) optimal linear layer quantization. arXiv:2603.04956. Cited by: §9. [10] J. Lin, J. Tang, H. Tang, S. Yang, W. Chen, W. Wang, G. Xiao, X. Dang, C. Gan, and S. Han (2024) AWQ: activation-aware weight quantization for LLM compression and acceleration. In MLSys, Note: arXiv:2306.00978 Cited by: §9. [11] H. Park, G. Lee, T. Piao, and T. Kim (2026) Value-and-structure alignment for routing-consistent quantization of mixture-of-experts models. arXiv:2606.05688. Note: the method is named VSRAQ Cited by: §9. [12] Z. Su, Z. Zhang, T. Lan, Z. Wang, H. Shen, J. Yang, and Y. Cheng (2025) MorphServe: efficient and workload-aware LLM serving via runtime quantized layer swapping and KV cache resizing. arXiv:2506.02006. Cited by: §9. [13] A. Tseng, Z. Sun, and C. De Sa (2026) Model-preserving adaptive rounding. In ICML, Note: arXiv:2505.22988; the method is named YAQA Cited by: §9. [14] F. Wei, L. Liu, Z. Wang, and C. Wang (2026) Runtime observability for heterogeneous attention memory. arXiv:2608.05863. Cited by: §2. [15] F. Wei, L. Liu, Z. Wang, and C. Wang (2026) WitCert: sound runtime risk observability and gating for KV-cache quantization. arXiv:2607.28699. Cited by: §2, §9. [16] C. Zhang, J. T. H. Wong, C. Xiao, G. A. Constantinides, and Y. Zhao (2025) QERA: an analytical framework for quantization error reconstruction. In ICLR, Note: arXiv:2410.06040 Cited by: §9. [17] Z. Zhao, Z. Xu, Z. Chen, and D. Yang (2026) MoBiE: efficient inference of mixture of binary experts under post-training quantization. Note: arXiv:2604.06798withdrawn by the authors, 20 Apr 2026 Cited by: §9.