Eq. (4.25) — quantum Singleton bound $m\ge (n+k)/2$ for symmetric erasure codes

Proved

HarlowTASI.quantum_singleton_bound

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

holographyoperator-algebrasquantum-error-correctionquantum-information

Encode $k\ge1$ logical qudits into $n$ physical qudits, each of dimension $d\ge2$ : the code subspace is the image of an isometry $V:(\mathbb C^d)^{\otimes k}\to(\mathbb C^d)^{\otimes n}$ . Say that the logical information is accessible from a set $A$ of physical qudits if every logical operator $\tilde O$ has a representative $O_A$ supported on $A$ with $O_A|\tilde\psi\rangle=\tilde O|\tilde\psi\rangle$ and $O_A^\dagger|\tilde\psi\rangle=\tilde O^\dagger|\tilde\psi\rangle$ for all code states (condition (1) of Theorem 4.1 with $R=A$ ). Assume, as in the lectures, that whether a set of qudits gives access to the logical information depends only on the number of qudits in it. Then every set $A$ from which the information is accessible satisfies

|A|\ \ge\ \frac{n+k}{2};

equivalently, the smallest such number $m$ obeys the quantum Singleton bound $m\ge\frac{n+k}{2}$ (4.25).

This bound quantifies how large a code subspace can be while remaining correctable, and in the lectures it is checked against the three-qutrit code ( $n=3$ , $k=1$ , $m=2$ ).

Formalization Note Qudits are indexed by Fin n, a set of qudits is a Finset (Fin n), and the symmetry assumption is stated as: any two sets of equal cardinality are either both accessible or both not. The hypotheses $d\ge2$ and $k\ge1$ are implicit in the lectures (a qudit is a $d$ -state system carrying information; for $d=1$ or $k=0$ the code space is one-dimensional, everything is accessible from the empty set, and the bound fails).

Preamble

import Mathlib
import Definitions.Def_HarlowTASI_QuantumBasics

Formal statement

namespace HarlowTASI
theorem quantum_singleton_bound {n d k : ℕ} (hd : 2 ≤ d) (hk : 1 ≤ k)
    (V : Matrix (Fin n → Fin d) (Fin k → Fin d) ℂ) (hV : IsIsometry V)
    (hsymm : ∀ A B : Finset (Fin n), A.card = B.card →
      (AccessibleFrom V A ↔ AccessibleFrom V B))
    (A : Finset (Fin n)) (hA : AccessibleFrom V A) :
    n + k ≤ 2 * A.card := by sorry
end HarlowTASI

Source

Daniel Harlow, TASI Lectures on the Emergence of Bulk Physics in AdS/CFT, PoS(TASI2017)002 (2018), arXiv:1802.01040, §4.3, pp. 29–30, eqs. (4.21)–(4.25) (quantum Singleton bound).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - NON-BLIND: same agent that drafted the statements

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source lectures and of the intended meaning. It was not produced blind by an independent auditor, so it must not be mistaken for independent testimony; reviewers should treat it as the drafter's own rendering of the code and check the Lean text directly.

Data. Natural numbers $n,d,k$ with $d\ge2$ and $k\ge1$ ; a complex matrix $V$ whose rows are indexed by functions $x:\{0,..,n-1\}\to\{0,..,d-1\}$ (so $d^n$ rows) and whose columns are indexed by functions $\{0,..,k-1\}\to\{0,..,d-1\}$ ( $d^k$ columns), assumed an isometry: $V^\dagger V=I$ .

Symmetry hypothesis. For all subsets $A,B\subseteq\{0,..,n-1\}$ with $|A|=|B|$ : $V$ is accessible from $A$ iff it is accessible from $B$ . Here "accessible from $A$ " means: for every $d^k\times d^k$ matrix $O$ there is a matrix $O_A$ indexed by functions $A\to\{0,..,d-1\}$ with $(O_A\otimes I_{A^c})\,\mathrm{split}_AV=\mathrm{split}_AV\,O$ and $(O_A^\dagger\otimes I_{A^c})\,\mathrm{split}_AV=\mathrm{split}_AV\,O^\dagger$ , where $\mathrm{split}_AV$ is $V$ with each row index $x$ rewritten as the pair (restriction of $x$ to $A$ , restriction of $x$ to the complement of $A$ ).

Claim. For every subset $A\subseteq\{0,..,n-1\}$ from which $V$ is accessible,

n+k\le 2\,|A| .

Edge remarks: for $n=0$ there is a single row, and an isometry with $d^k\ge2$ columns cannot exist, so the statement is then vacuous; for $n\ge1$ the hypotheses are satisfiable (e.g. by codes with the stated symmetry). The full set $A=\{0,..,n-1\}$ is always accessible when $V$ is an isometry, so the claim includes $k\le n$ .

Human review

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

View graph

Eq. (4.25) — quantum Singleton bound m≥(n+k)/2m\ge (n+k)/2m≥(n+k)/2 for symmetric erasure codes

Eq. (4.25) — quantum Singleton bound $m\ge (n+k)/2$ for symmetric erasure codes