Exact distances and measurement allocation for logical Pauli readout
Shuoming An, Fusheng Yang
quant-ph
Oct 3, 2026 · v2
TL;DR
Lean certifies finite distance values, algebraic and finite-code results, and five arithmetic resource-count lemmas; the formal development is archived on Zenodo.
Abstract
The minimum fault weight of a logical readout depends jointly on data-error persistence, check redundancy and time-boundary constraints. For any binary check matrix $H$ and nonzero parity support $w$, we prove that a repeated-readout model with a zero-syndrome endpoint has exact distance $\min_{w\cdot y=1}[\operatorname{wt}(y)+q\operatorname{wt}(Hy)]$ for at least $q$ wrong readouts. This reduces the search over fault histories to one weighted spatial minimum and gives the minimum repetition count for each adjacent-column check in square Bacon–Shor and generalized Shor readouts. Combining those checks with redundant Gauss-check pair products yields an exact joint distance and an outcome-count optimum within the specified gauged-readout family. At target distance $m$, one round uses $m^2$ outcomes, compared with $m(2m-1)$ for the repeated baseline in the same phenomenological model. For a one-epoch bare-ancilla CNOT implementation, we prove a schedule-dependent distance upper bound by constructing an accepted wrong readout from one gate fault and outcome flips. The bound identifies necessary timing conditions for retaining the target distance and gives matching upper bounds of three for the best tested schedules at both $m=3$ and $m=5$.
Problem
The minimum fault weight of a logical Pauli readout in quantum error correction depends on data-error persistence, check redundancy and time-boundary constraints. It was unclear how these factors set the exact distance and how to allocate measurements to reach a target distance.
Approach
For any binary check matrix H and parity support w, the authors prove that the repeated-readout model with a zero-syndrome endpoint has exact distance min over w·y=1 of [wt(y)+q·wt(Hy)]. This yields minimal repetition counts for adjacent-column checks in Bacon–Shor and generalized Shor readouts. They combine these checks with redundant Gauss-check pair products for gauged readout, and they bound the distance of bare-ancilla CNOT schedules by constructing faults. Finite values, algebraic results and resource-count arithmetic lemmas are certified in Lean, alongside independent dynamic programs and Pauli-propagation checks.
Results
At target distance m, one round uses m^2 outcomes, compared with m(2m-1) for the repeated baseline in the same phenomenological model. The schedule-dependent bound gives matching upper bounds of three for the best tested schedules at both m=3 and m=5. Twelve nine-qubit readout distances are certified in Lean.
| Model | Error criterion | Distances (T=1..4) |
|---|
| Measurement only | Constant logical flip | 1,2,3,4 |
| Persistent faults | Strict majority | 2,3,3,3 |
| No boundary constraint | Strict majority | 1,1,1,1 |
| Last-round control | Last readout wrong | 2,2,2,2 |
Nine-qubit Bacon–Shor readout models and exact distances at T=1,2,3,4 (first three rows certified in Lean)