The verifier side of speculative window decoding: a predictability bracket, a machine-checked blast-radius bound, and a decoder-agnostic recover loop
Rylan Malarchick
quant-ph
Jul 7, 2026 · v2
cs.AR
TL;DR
The probability core of the temporal blast-radius bound (Peierls/union-bound tail, path-count bound) is machine-checked in Lean 4 with Mathlib.
Abstract
Speculative window decoders hide quantum error-correction decoder latency by guessing the cross-boundary decisions that link adjacent decoding windows, running downstream work on the guess, and verifying lazily. SWIPER and ARTERY each build one predictor, about 90% accurate; neither built the verifier side. We build it on a reconstructed SWIPER harness (Stim rotated surface code, minimum-weight matching). A predictor-only bracket shows the cross-boundary decision is local, the achievable accuracy reaching about 0.999 within three rounds, with small, diffuse headroom over SWIPER. We establish a worst-case temporal blast-radius bound, its probability core machine-checked in Lean4 and conditional on a modeling reduction we then test: a misprediction's effect decays exponentially in the commit width, so the radius is one and speculation adds no error floor. We falsify that reduction shot by shot and find the real mechanism, clearest at near-threshold noise, is a global minimum-weight re-pairing. A compiler pass derives SWIPER's restart policy from these numbers; a runtime executor confirms on the harness that the loop recovers exactly and removes the serial commit-chain stall up to a small penalty. A second decoder (union-find) settles which results are decoder-agnostic: the predict-verify-recover wrapper and the structural phenomenology, while the absolute magnitudes and the min-weight mechanism are matching-specific.
Problem
Speculative window decoders for quantum error correction (SWIPER, ARTERY) build predictors for cross-boundary decisions but no verifier side. Open questions are the achievable prediction accuracy, how far a misprediction can corrupt later windows, when speculation pays off, and whether a full predict-verify-recover loop works on a real decoder.
Approach
A SWIPER harness is reconstructed with Stim rotated surface codes and PyMatching MWPM. Achievable accuracy is bracketed with local-MWPM and learned predictors. A worst-case temporal blast-radius bound is proved, with its probability core (union-bound tail, path-count bound, assembled conditional containment theorem) machine-checked in Lean 4 with Mathlib and no sorry; the path-count bound was closed with the Aristotle prover. The bound's modeling reduction is then tested shot by shot, and the results feed a compiler pass and a runtime executor, which are cross-checked against a union-find decoder.
Results
The boundary decision is local: accuracy reaches about 0.999 within three rounds, and headroom over SWIPER is 0.019–0.063. Propagation decays exponentially in commit width, giving a temporal blast radius of one. The shot-by-shot tests falsify the Lean theorem's reduction hypothesis; the actual mechanism is a global minimum-weight re-pairing. On a 16-window chain the executor recovers exactly and reaches speedups of about 15.99–16.00.
| d | W | Restart rate | Speedup | Speedup (pred=0.7) |
|---|
| 7 | 1 | 8.9e-3 | 15.999 | 15.80 |
| 7 | 3 | 1.0e-4 | 16.000 | 15.99 |
| 9 | 1 | 1.3e-2 | 15.997 | 15.81 |
| 9 | 3 | 3.2e-4 | 16.000 | 15.99 |
Executor on a 16-window chain, p=1e-3 (subset)
