Quantum Gilbert–Varshamov, quantum Hamming, and asymptotic rate bounds

Open

QAlgorithms.GottesmanIntro.codeBounds

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

gottesman-introlecture-notesquantum-information

An $[[n,k,d]]$ code is a subspace $C$ of $(\mathbb C^2)^{\otimes n}$ of dimension $2^k$ such that every operator $E$ acting on at most $d-1$ qubits satisfies $\langle\psi|E|\psi\rangle=c'(E)$ for all unit vectors $|\psi\rangle\in C$ , with $c'(E)$ independent of $|\psi\rangle$ (eq. (34)); that is, $C$ has distance at least $d$ . Put $t=\lfloor (d-1)/2\rfloor$ . The code is nondegenerate if, for every unit vector $|\psi\rangle\in C$ , the Gram matrix $\big(\langle\psi|P_a^\dagger P_b|\psi\rangle\big)_{a,b}$ over the phase-free Pauli operators $P_a$ of weight at most $t$ is nonsingular. Let $H(x)=-x\log_2x-(1-x)\log_2(1-x)$ .

(Quantum Gilbert–Varshamov bound.) If $d\ge1$ and

\Big(\sum_{j=0}^{d-1}3^j\binom nj\Big)2^k\le 2^n,

then an $[[n,k,d]]$ code exists. 2. (Quantum Hamming bound.) Every nondegenerate $[[n,k,d]]$ code satisfies

\Big(\sum_{j=0}^{t}3^j\binom nj\Big)2^k\le 2^n.

(Asymptotic rates.) Let $0<p<1/2$ $0 < p < 1/2$ and $\varepsilon>0$ $ε > 0$ . There is $N$ $N$ such that for every $n\ge N$ $n \geq N$ :
- every nondegenerate $[[n,k,d]]$ code with $d\ge 2pn$ has $k/n\le 1-p\log_2 3-H(p)+\varepsilon$ ;
- if $1-2p\log_2 3-H(2p)>0$ , there is a nondegenerate $[[n,k,d]]$ code with $d\ge 2pn$ and $k/n\ge 1-2p\log_2 3-H(2p)-\varepsilon$ .

The first two bounds are counting arguments. The third gives the rate window, eq. (37), between which the best nondegenerate codes lie.

Formalization Note The source's 'distance $d$ ' is read as distance at least $d$ , so existence is meaningful also for $k=0$ . The hypothesis $d\ge1$ excludes $d=0$ , where (36) is an empty sum and the claim would demand a $2^k$ -dimensional code for every $k$ . The asymptotic clause is read as an $\varepsilon$ – $N$ statement. The lower rate bound is asserted only when it is positive.

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro

open scoped Matrix

open QAlgorithms Stabilizer




/-- Gottesman intro p.7–8, Theorem 4. (1) Quantum Gilbert–Varshamov: if
`(∑_{j=0}^{d-1} 3^j C(n,j)) 2^k ≤ 2^n` (eq. (36)) and `d ≥ 1`, an `[[n, k, d]]` code exists.
(2) Quantum Hamming bound: every nondegenerate `[[n, k, d]]` code satisfies
`(∑_{j=0}^{t} 3^j C(n,j)) 2^k ≤ 2^n` (eq. (35)), `t = ⌊(d-1)/2⌋`. (3) Asymptotics (eq. (37)):
for fixed `p ∈ (0, 1/2)` and every `ε > 0`, for all large `n`, every nondegenerate `[[n, k, d]]`
code with `d ≥ 2pn` has `k/n ≤ 1 - p log₂ 3 - H(p) + ε`, and, when `1 - 2p log₂ 3 - H(2p) > 0`,
some nondegenerate `[[n, k, d]]` code with `d ≥ 2pn` has `k/n ≥ 1 - 2p log₂ 3 - H(2p) - ε`. -/
theorem codeBounds :
    (∀ n k d : ℕ, 1 ≤ d →
      (∑ j ∈ Finset.range d, 3 ^ j * n.choose j) * 2 ^ k ≤ 2 ^ n →
      ∃ C : Submodule ℂ (EuclideanSpace ℂ (Qubits n)), IsQCode n k d C) ∧
    (∀ (n k d : ℕ) (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))), IsQCode n k d C →
      IsNondegenerate C ((d - 1) / 2) →
      (∑ j ∈ Finset.range ((d - 1) / 2 + 1), 3 ^ j * n.choose j) * 2 ^ k ≤ 2 ^ n) ∧
    ∀ p : ℝ, 0 < p → p < 1 / 2 → ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n ≥ N,
      (∀ (k d : ℕ) (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))), IsQCode n k d C →
        IsNondegenerate C ((d - 1) / 2) → 2 * p * n ≤ d →
        (k : ℝ) / n ≤ 1 - p * Real.logb 2 3 - binEntropy2 p + ε) ∧
      (0 < 1 - 2 * p * Real.logb 2 3 - binEntropy2 (2 * p) →
        ∃ (k d : ℕ) (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))), IsQCode n k d C ∧
          IsNondegenerate C ((d - 1) / 2) ∧ 2 * p * n ≤ d ∧
          1 - 2 * p * Real.logb 2 3 - binEntropy2 (2 * p) - ε ≤ (k : ℝ) / n) := by
  sorry

end QAlgorithms.GottesmanIntro

Source

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

Read-back

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

Codes. For $n,k,d\in\mathbb{N}$ , " $C$ is an $[[n,k,d]]$ code" means $C$ is a complex subspace of the $n$ -qubit space $\mathbb{C}^{\{0,1\}^n}$ satisfying two conditions.

$\dim_{\mathbb{C}}C=2^k$ .
Every complex matrix $E$ acting on at most $d-1$ qubits is detectable, i.e. there is a constant $c\in\mathbb{C}$ with $\langle\psi,E\psi\rangle=c$ for all unit $\psi\in C$ .

Two clarifications:

Acting on few qubits. " $E$ acts on at most $s$ qubits" means $E=M\otimes I$ for an arbitrary matrix $M$ placed on some set of at most $s$ wires, as in the previous entry.
Truncated subtraction. $d-1$ is truncated, so $d=0$ behaves like $d=1$ . In that case only scalar multiples of the identity must be detected, which always holds.

The condition says "distance at least $d$ ". It does not say the distance is exactly $d$ .

Nondegeneracy. Write $\mathcal{P}_t$ for the phase-free Pauli products $\sigma_1\otimes\cdots\otimes\sigma_n$ ( $\sigma_q\in\{I,X,Y,Z\}$ ) with at most $t$ non-identity factors. " $C$ is nondegenerate at $t$ " means: for every unit $\psi\in C$ , the Gram matrix

\big(\langle P\psi,\,Q\psi\rangle\big)_{P,Q\in\mathcal{P}_t}

has nonzero determinant. Equivalently, the vectors $P\psi$ , $P\in\mathcal{P}_t$ , are linearly independent.

Notation.

$H_2(p)=\dfrac{-p\ln p-(1-p)\ln(1-p)}{\ln 2}$ is the binary entropy in bits.
$\lfloor (d-1)/2\rfloor$ uses truncated subtraction and floor division of natural numbers.

The theorem is a conjunction of three statements.

Existence (Gilbert–Varshamov form). Let $n,k,d\in\mathbb{N}$ with $d\ge 1$ . If

\Big(\sum_{j=0}^{d-1}3^j\binom{n}{j}\Big)\cdot 2^k\le 2^n,

then some subspace $C$ is an $[[n,k,d]]$ code.

Hamming bound. Let $n,k,d\in\mathbb{N}$ and $t=\lfloor(d-1)/2\rfloor$ . Every $[[n,k,d]]$ code $C$ that is nondegenerate at $t$ satisfies

\Big(\sum_{j=0}^{t}3^j\binom{n}{j}\Big)\cdot 2^k\le 2^n.

Asymptotic rates. For every real $p$ with $0<p<\tfrac12$ and every real $\varepsilon>0$ , there exists $N\in\mathbb{N}$ such that every $n\ge N$ satisfies both (i) and (ii).

(i) Upper bound. For all $k,d$ and every $[[n,k,d]]$ code $C$ that is nondegenerate at $\lfloor(d-1)/2\rfloor$ and has $2pn\le d$ :

\frac{k}{n}\le 1-p\log_2 3-H_2(p)+\varepsilon.

(ii) Achievability. Suppose

1-2p\log_2 3-H_2(2p)>0.

Then there exist $k,d$ and an $[[n,k,d]]$ code $C$ that is nondegenerate at $\lfloor(d-1)/2\rfloor$ , has $2pn\le d$ , and satisfies

1-2p\log_2 3-H_2(2p)-\varepsilon\le\frac{k}{n}.

Here $k/n$ is real division. If $n=0$ were allowed (i.e. $N=0$ ), $k/0$ evaluates to $0$ .

When $2p\ge 1$ , the term $H_2(2p)$ is evaluated by the same total formula: $H_2(1)=0$ and, for $2p>1$ , logarithms of negative arguments are taken as $\ln|x|$ . However, $2p<1$ holds here because $p<\tfrac12$ .

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