The quantum capacity of the erasure channel is max(0, 1 − 2p)

Open

QAlgorithms.GottesmanThesis.erasureChannel_capacity

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

gottesman-thesislecture-notesquantum-information

Fix an erasure probability $p \in [0,1]$ . The qubit erasure channel $\mathcal N_p$ acts independently on each qubit sent: with probability $1-p$ the qubit passes unchanged together with a classical flag $0$ , and with probability $p$ it is replaced by the maximally mixed state $I/2$ together with the flag $1$ , so that the receiver knows which qubits were erased. On $n$ qubits the channel is $\mathcal N_p^{\otimes n}$ .

A rate $R \in \mathbb R$ is achievable (for quantum codes, equivalently one-way entanglement purification) if for every $\varepsilon > 0$ and $\delta > 0$ there is $N_0$ such that for every $n \ge N_0$ there are a number $k \ge (R-\delta)n$ of logical qubits, an encoding quantum channel $\mathcal E$ from $k$ qubits to $n$ qubits and a decoding quantum channel $\mathcal D$ from the channel output (qubits and erasure flags) to $k$ qubits with

F_e\big(\mathcal D \circ \mathcal N_p^{\otimes n} \circ \mathcal E\big) \ge 1 - \varepsilon,

where $F_e(\Phi) = \langle \Phi_k | (\mathrm{id} \otimes \Phi)(|\Phi_k\rangle\langle \Phi_k|) | \Phi_k \rangle$ is the entanglement fidelity with respect to the maximally entangled state $|\Phi_k\rangle$ of two $k$ -qubit registers. The theorem states that the quantum capacity of the erasure channel is $\max(0, 1-2p)$ , in the strong form that the set of achievable rates is exactly

\{R : R \text{ achievable for } \mathcal N_p\} = \big(-\infty,\ \max(0, 1-2p)\big].

In particular every rate below $1-2p$ is achievable (random stabilizer codes), no rate above $1-2p$ is (a no-cloning argument), and for $p \ge 1/2$ the capacity is zero.

Formalization Note The supremum of achievable rates is not written as a real sSup (which would be junk on an empty or unbounded set); instead the achievable set itself is characterized. Because the definition of achievability already has the slack $\delta$ , the achievable set is closed, so the capacity $\max(0,1-2p)$ is itself an achievable rate. The author's errata note that the thesis's proof of the upper bound assumes there is no superadditivity when a noiseless channel is added to a zero-rate channel; the theorem itself is the established value (Bennett–DiVincenzo–Smolin).

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanThesis

/-- Gottesman thesis §7.5, pp.90–91 (unnumbered): the quantum capacity of the qubit erasure
channel with erasure probability `p` is `max(0, 1 − 2p)`.

The erasure channel (frozen `erasureChannel n p`) acts independently on each of the `n` qubits:
with probability `1 − p` the qubit passes unchanged with flag `0`, with probability `p` it is
replaced by the maximally mixed state with flag `1`, so the receiver knows which qubits were
erased. A rate `R` is achievable (frozen `IsAchievableQRate`) when for all `ε, δ > 0` and all large
`n` there are an encoding channel of `k ≥ (R − δ) n` qubits into `n` qubits and a decoding channel
(seeing the flags) whose composite with the erasure channel has entanglement fidelity `≥ 1 − ε`
(the 1-EPP picture of §7.4; no classical feedback). The capacity being `max(0, 1 − 2p)` is stated
as: the achievable rates are exactly the `R ≤ max(0, 1 − 2p)` (the δ-slack in the definition makes
the set of achievable rates closed, so the supremum is attained).

Erratum (author's errata page): the thesis's proof of the upper bound `1 − 2p` assumes no
superadditivity when a noiseless channel is added to a zero-rate channel; the value itself is the
established one (Bennett–DiVincenzo–Smolin), and is stated unchanged. -/
theorem erasureChannel_capacity (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (R : ℝ) :
    IsAchievableQRate (fun n => erasureChannel n p) R ↔ R ≤ max 0 (1 - 2 * p) := by
  sorry

end QAlgorithms.GottesmanThesis

Source

Daniel Gottesman, Stabilizer Codes and Quantum Error Correction, 1997 thesis, downloaded arXiv v1 PDF; PDF title page now prints 2024, PDF p. 90, §7.5. https://arxiv.org/pdf/quant-ph/9705052v1

Read-back

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

Statement. Let $p$ be a real number with $0 \le p \le 1$ , and let $R$ be any real number (negative values included). Then

R \text{ is an achievable quantum rate for the family } (\mathcal{E}^{(n)}_p)_{n\in\mathbb N} \iff R \le \max\{0,\ 1-2p\}.

In particular, for $p \ge 1/2$ the right-hand side reads $R \le 0$ .

The channel $\mathcal{E}^{(n)}_p$ . The single-qubit map has input a qubit (basis $\{0,1\}$ ) and output a pair $(a,f)\in\{0,1\}\times\{0,1\}$ : a qubit $a$ together with a flag bit $f$ . It has five Kraus operators, each a $4\times 2$ matrix:

$K_0 = \sqrt{1-p}\,\sum_b |b,0\rangle\langle b|$ . The state is passed through unchanged and the flag is set to $0$ .
$K_{a,c} = \sqrt{p/2}\,|a,1\rangle\langle c|$ for each of the four pairs $a,c\in\{0,1\}$ .

With the flag set to $1$ , the four operators $K_{a,c}$ together produce $p\,\operatorname{Tr}(\rho)\cdot \tfrac{I}{2}\otimes|1\rangle\langle 1|$ . So an "erasure" is represented by the maximally mixed qubit with flag $1$ , not by a separate erasure symbol.

The $n$ -qubit channel $\mathcal{E}^{(n)}_p$ maps $n$ -qubit matrices to matrices indexed by $(\{0,1\}\times\{0,1\})^n$ . It is defined by

\mathcal{E}^{(n)}_p(\rho) = \sum_{j\in\{0,\dots,4\}^n} K_j\,\rho\,K_j^\dagger, \qquad (K_j)_{y,z} = \prod_{q=1}^{n} \big(K_{j_q}\big)_{y_q,z_q},

which is the $n$ -fold tensor power of the single-qubit map. The definition itself takes $\sqrt{\cdot}$ of $1-p$ and $p/2$ . The hypothesis $0\le p\le1$ keeps both square-root arguments nonnegative.

Achievable rate. A quantum channel from $\iota$ to $\kappa$ is a map $\Phi$ on matrices for which there exist finitely many matrices $E_1,\dots,E_m$ such that:

$\sum_i E_i^\dagger E_i = I$ , and
$\Phi(\rho)=\sum_i E_i\rho E_i^\dagger$ for every matrix $\rho$ .

The rate $R$ is achievable when the following holds. For every $\varepsilon>0$ and every $\delta>0$ there is an $N_0$ such that for every $n\ge N_0$ there exist:

a natural number $k$ with $(R-\delta)\,n \le k$ (no upper bound on $k$ is imposed, and $k=0$ is allowed),
a quantum channel $\mathrm{Enc}$ from $k$ qubits to $n$ qubits, and
a quantum channel $\mathrm{Dec}$ from the output space $(\{0,1\}\times\{0,1\})^n$ to $k$ qubits,

such that

1-\varepsilon \le F_e\big(\mathrm{Dec}\circ\mathcal{E}^{(n)}_p\circ\mathrm{Enc}\big).

Entanglement fidelity. For a map $\Phi$ on $k$ -qubit matrices, $F_e(\Phi)$ is defined as follows. Take the maximally entangled vector on two copies of the $k$ -qubit register (reference copy first):

|\Phi_k\rangle = 2^{-k/2}\sum_{x\in\{0,1\}^k}|x,x\rangle .

Then

F_e(\Phi) = \operatorname{Re}\,\langle\Phi_k|\,(\mathrm{id}\otimes\Phi)\big(|\Phi_k\rangle\langle\Phi_k|\big)\,|\Phi_k\rangle .

Here $\mathrm{id}\otimes\Phi$ applies $\Phi$ to each block of the matrix indexed by the reference register.

Edge cases.

When $k=0$ , the register is a single basis state.
Any $R\le 0$ satisfies the bound $(R-\delta)n\le k$ with $k=0$ .
The real number $R$ is unrestricted, so the equivalence also covers all negative $R$ ; for those, the right-hand side holds automatically.

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