Better gates: one level of encoding gives error $O(p^2)$ per location

Open

ThresholdTheorem.level_one_error_suppression

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

fault-tolerancequantum-computingquantum-error-correction

Better gates from error-correcting codes (one level of encoding). There are constants $c>0$ and $A$ , a block size $b$ and a decoder $\mathrm{dec}:\{0,1\}^b\to\{0,1\}$ such that every ideal circuit $C$ on $n$ qubits has a physical simulation $C'$ on $n$ blocks of $b$ qubits with $|C'|\le A\,|C|$ and, for every $0\le p$ with $cp<1$ and every independent stochastic noise model with fault rate at most $p$ ,

d_{\mathrm{TV}}\big(\mathrm{dec}_*P_{\mathrm{noisy}}(C'),\,P_{\mathrm{ideal}}(C)\big)\;\le\;c\,p^{2}\,|C| .

Compared with the unencoded bound $p\,|C|$ , each simulated location now fails with probability $O(p^2)$ instead of $O(p)$ : the encoded gates are larger, but because of error correction they fail less often than the original gates once $p$ is small.

Preamble

import Mathlib
import Definitions.Def_threshold_theorem_noise_model

open ThresholdTheorem

Formal statement

namespace ThresholdTheorem
theorem level_one_error_suppression :
    ∃ (c A : ℝ) (b : ℕ) (dec : (Fin b → Fin 2) → Fin 2), 0 < c ∧
      ∀ (n : ℕ) (C : Circuit (Fin n)), ∃ C' : Circuit (Fin n × Fin b),
        (C'.size : ℝ) ≤ A * C.size ∧
        ∀ (p : ℝ), 0 ≤ p → c * p < 1 → ∀ N : NoiseModel p,
          tvDist (decodeDist dec (outDist (noisyState N C'))) (outDist (idealState C))
            ≤ c * p ^ 2 * C.size := by sorry
end ThresholdTheorem

Source

Wikipedia, "Threshold theorem" (revision oldid=1360742213, https://en.wikipedia.org/w/index.php?title=Threshold_theorem&oldid=1360742213), section "Explanation"; the boxed statement is quoted there from M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, 10th anniversary ed., Cambridge University Press, p. 481.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Better gates: one level of encoding gives error O(p2)O(p^2)O(p2) per location

Better gates: one level of encoding gives error $O(p^2)$ per location