Level reduction: a local stochastic model on C′ induces one on C with bounds Σ_{|R|=t+1} Π p_j

Open

QAlgorithms.GottesmanIntro.level_reduction

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

gottesman-introlecture-notesquantum-information

Fix an $[[n,1,2t+1]]$ code with fault-tolerant gadgets of a common depth (Definitions 2–5), a circuit $C$ as in Definition 6, and its fault-tolerant circuit $C'$ . Suppose $C'$ undergoes a local stochastic error model (Definition 12): with probability $p_S$ the faults are at precisely the set $S$ of locations of $C'$ , the errors there being arbitrary quantum operations, possibly entangled through an environment, applied in chronological order; and for every set $R$ of locations,

\sum_{S\supseteq R} p_S \le \prod_{j\in R} p_j,\qquad p_j<1.

For a location $C_i$ of $C$ put

p'_i = \sum_{R} \prod_{j\in R} p_j,

the sum over the sets $R$ of exactly $t+1$ locations of $C'$ contained in the extended rectangle of $C_i$ . Then there is an error model on $C$ such that

faults occur at precisely the set $S'$ of locations of $C$ with probability $\sum_{S:\,\mathrm{bad}(S)=S'} p_S$ , where $\mathrm{bad}(S)$ is the set of bad ExRecs assigned by Definition 10;
the decoded output distribution of $C'$ equals the output distribution of $C$ under this model;
the model is local stochastic with error bounds $p'_i$ : for every set $R$ of locations of $C$ , the probability of faults at all of $R$ is at most $\prod_{i\in R} p'_i$ ;
if $0\le p$ and $p_j\le p$ for all locations $j$ of $C'$ , then $p'_i\le A\,p^{t+1}$ for every location $C_i$ , where $A$ is the maximum over the types of ExRecs of the number of $(t+1)$ -element sets of locations of the ExRec.

This is the step that lets concatenation reduce the error rate from $p$ to $A p^{t+1}$ per level.

Formalization Note The side condition $p'_i<1$ of Definition 12 is not claimed (eq. (84) can exceed $1$ ); the local stochastic inequality is stated with the bounds $p'_i$ exactly.

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
import Definitions.Def_QAlgorithms_GottesmanIntro_Ch05b_Model
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro





/-- Gottesman intro p.40, Theorem 9 (Level Reduction): "Suppose we have a fault-tolerant circuit
`C′` for `C`, and suppose `C′` experiences a local stochastic error model with error bounds `p_i`
and probability `p_S` of errors at precisely the set `S` of locations. Then for any particular set
`S` define `C̃_S` as in theorem 8, and define an error model on `C` by replacing `C` with `C̃_S`
with probability `p_S`. This is a local stochastic error model. The error bounds `p′_i` for `C`
are given by `p′_i ≤ Σ_R Π_{i∈R} p_i` (84) … In the special case where `p_i ≤ p` for all `i`, we
have `p′_i ≤ A p^{t+1}` (85)."

Let `P` be a fault-tolerant protocol, `C` a Def. 6 circuit, and `M` a local stochastic error
model (Def. 12: arbitrary chronological quantum errors, possibly entangled through an environment,
at a random set of faulty locations) on `C′ = ftCircuit P C` with bounds `p_i < 1`. Then there is
an error model `M′` on `C` such that
1. faults occur at precisely the set `S′` of locations of `C` with probability
   `Σ_{S : bad(S) = S′} p_S`, `bad(S)` the bad locations of Def. 10;
2. the decoded output distribution of `C′` under `M` equals the output distribution of `C` under
   `M′`;
3. `M′` is local stochastic with the bounds `p′_i` of eq. (84);
4. if `0 ≤ p` and `p_j ≤ p` for every location `j` of `C′`, then `p′_i ≤ A p^{t+1}` for every location `i`
   of `C`, with `A` as in eq. (85). -/
theorem level_reduction (P : FTProtocol) (hP : P.IsFaultTolerant) (hdepth : P.HasUniformDepth)
    {N : ℕ} (C : LocCircuit N) (hC : C.IsIdealCircuit)
    (M : LocalStochasticModel (N * (P.n + P.A))) (p : ℕ × ℕ → ℝ)
    (hp1 : ∀ j ∈ (ftCircuit P C).locs, p j < 1) (hM : IsLocalStochastic (ftCircuit P C) M p) :
    ∃ M' : LocalStochasticModel N,
      (∀ S' : Finset (ℕ × ℕ), M'.prob S' =
        ∑ S ∈ (ftCircuit P C).locs.powerset.filter (fun S => badAssignment P C S = S'),
          M.prob S) ∧
      pushDist (ftDecode P C) (noisyOutDist (ftCircuit P C) M) = noisyOutDist C M' ∧
      IsLocalStochastic C M' (levelReducedBound P C p) ∧
      ∀ p0 : ℝ, 0 ≤ p0 → (∀ j ∈ (ftCircuit P C).locs, p j ≤ p0) →
        ∀ i ∈ C.locs, levelReducedBound P C p i ≤ (exRecSubsetMax P : ℝ) * p0 ^ (P.t + 1) := by
  sorry


end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 40, Theorem 9. https://arxiv.org/pdf/0904.2557v1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Data. The statement uses the same notions as the previous read-back. These are repeated here in compact form.

$P$ is a protocol $(n,t,A,\mathcal C,\mathrm{enc},\mathcal D,G_\kappa,G_{ec},\mathrm{measDecode})$ . It is assumed to be fault tolerant, which means all of the following:

$\mathcal C$ is a 2-dimensional code on which every operator supported on $\le 2t$ qubits is detectable.
$\mathrm{enc}$ is an isometry onto $\mathcal C$ .
$\mathcal D$ is a Kraus channel that ideally decodes $E\,\mathrm{enc}\,\psi$ for every $E$ in the span of weight- $\le t$ Pauli strings, giving $\|E\,\mathrm{enc}\,\psi\|^2|\psi\rangle\langle\psi|$ .
The gadgets and the EC circuit are well formed with the stated live data wires.
The Meas, Prep A/B, Gate A/B (for $H$ , $T$ , CNOT, wait) and EC A/B identities hold. Each is stated with the filters $\mathcal F_r$ , which conjugate by the projection onto $\mathrm{span}\{Pc:\mathrm{wt}(P)\le r,\ c\in\mathcal C\}$ , whenever the gadget's fault count plus the filter parameters is $\le t$ .

$P$ also has uniform gadget depth. $C$ is an ideal circuit on $N$ wires: well formed from no live wires to no live wires, with all conditions constantly true. $C'=\mathrm{FT}_P(C)$ is its fault-tolerant version on $N(n+A)$ wires, and $\mathrm{ftDecode}$ is its logical decoding of records.

Local stochastic models. A model $M$ on $N(n+A)$ wires consists of:

an environment dimension $e$ ;
a matrix $\sigma_0$ on the environment;
a real weight $\Pr_M(S)$ for every finite set $S$ of location ids;
superoperators $\mathcal E_S(\ell)$ on qubits $\otimes$ environment.

The noisy output distribution is

\mathrm{noisy}(C',M)(r)=\sum_{S\subseteq\mathrm{locs}(C')}\Pr_M(S)\;\mathrm{out}\big(C',\ \ell\mapsto[\ell\in S]\,\mathcal E_S(\ell),\ \sigma_0\big)(r).

Here $\mathrm{out}$ is $\operatorname{Re}\operatorname{Tr}$ of the classical–quantum run at record $r$ from $|0\cdots0\rangle\langle0\cdots0|\otimes\sigma_0$ .

A model is local stochastic with bound $b$ when:

$\sigma_0$ is a density matrix;
$\Pr(S)\ge0$ for all $S$ , and $\Pr(S)=0$ unless $S\subseteq\mathrm{locs}$ ;
$\sum_{S\subseteq\mathrm{locs}}\Pr(S)=1$ ;
for $\ell\in S$ at a location $l$ , $\mathcal E_S(\ell)$ is a channel on $l$ 's wires $\otimes$ environment, extended by the identity on the other wires;
for every $R\subseteq\mathrm{locs}$ ,

\sum_{R\subseteq S\subseteq\mathrm{locs}}\Pr(S)\le\prod_{i\in R}b(i).

Hypotheses. $M$ is local stochastic for $C'$ with bound $p$ , and $p(j)<1$ for every location $j$ of $C'$ .

The bad set. $\mathrm{Bad}(S)$ marks a location of $C$ as bad, scanning from the last step backwards, when more than $t$ elements of $S$ lie in its ExRec. The ExRec consists of its gadget, the leading EC on its wires (if it is not a preparation) and the trailing EC on its wires (if it is not a measurement). The trailing EC omits wires shared with a bad location of the next step.

Opaque quantities. The quantities $\mathrm{levelReducedBound}(P,C,p)$ , a function of location ids, and $\mathrm{exRecSubsetMax}(P)$ , a natural number, are not part of the provided definition layer. They are therefore not unfolded here.

Conclusion. There is a local stochastic model $M'$ on $N$ wires, with unconstrained environment dimension, initial environment and error superoperators, such that:

For every set $S'$ ,

\Pr_{M'}(S')=\sum_{S\subseteq\mathrm{locs}(C'),\ \mathrm{Bad}(S)=S'}\Pr_M(S).

The decoded noisy output of $C'$ equals the noisy output of $C$ under $M'$ :

\mathrm{push}_{\mathrm{ftDecode}}\,\mathrm{noisy}(C',M)=\mathrm{noisy}(C,M'),

where $\mathrm{push}_{\mathrm{dec}}\mu(r)=\sum_{\mathrm{dec}(r')=r}\mu(r')$ . 3. $M'$ is local stochastic for $C$ with bound $\mathrm{levelReducedBound}(P,C,p)$ . 4. For every real $p_0\ge0$ with $p(j)\le p_0$ at all locations $j$ of $C'$ , every location $i$ of $C$ satisfies

\mathrm{levelReducedBound}(P,C,p)(i)\le \mathrm{exRecSubsetMax}(P)\cdot p_0^{\,t+1}.

Human review

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

View graph