Theorem 4.1 — four equivalent characterizations of a correctable erasure

Proved

HarlowTASI.erasure_correction_tfae

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

holographyoperator-algebrasquantum-error-correctionquantum-information

Let $\mathcal H=\mathcal H_R\otimes\mathcal H_{\overline R}$ be finite-dimensional and let $\mathcal H_{code}\subseteq\mathcal H$ be a nonzero subspace with orthonormal basis $|\tilde i\rangle$ , $i\in C$ , and orthogonal projection $P$ . The following are equivalent:

For every operator $\tilde O$ on $\mathcal H_{code}$ there is an operator $O_R$ on $\mathcal H_R$ such that for all $|\tilde\psi\rangle\in\mathcal H_{code}$

O_R|\tilde\psi\rangle=\tilde O|\tilde\psi\rangle,\qquad O_R^\dagger|\tilde\psi\rangle=\tilde O^\dagger|\tilde\psi\rangle. \tag{4.16}

For every operator $X_{\overline R}$ on $\mathcal H_{\overline R}$ there is $\lambda\in\mathbb C$ with $PX_{\overline R}P=\lambda P$ . (4.17)
With a reference system $S$ of dimension $|S|=\dim\mathcal H_{code}$ and $|\phi\rangle=|S|^{-1/2}\sum_i|i\rangle_S|\tilde i\rangle_{R\overline R}$ (4.18), one has $\rho_{S\overline R}(\phi)=\rho_S(\phi)\otimes\rho_{\overline R}(\phi)$ . (4.19)
$|S|\le|R|$ , and for a decomposition $\mathcal H_R=(\mathcal H_{R_1}\otimes\mathcal H_{R_2})\oplus\mathcal H_{R_3}$ with $|R_1|=|S|$ and $|R_3|<|S|$ there are a unitary $U_R$ on $\mathcal H_R$ and a state $|\chi\rangle_{R_2\overline R}$ such that

|\tilde i\rangle_{R\overline R}=U_R\big(|i\rangle_{R_1}|\chi\rangle_{R_2\overline R}\big).\tag{4.20}

Theorem 4.1 is the basic structure theorem for erasure codes: condition (1) says that the encoded information can be reconstructed on $R$ , and (4) exhibits the encoding circuit. It is the subsystem-code special case of the mechanism behind Theorem 5.2, and it is the input of the quantum Singleton bound (4.25).

Formalization Note $\mathcal H_{code}$ is given by an isometry $V$ (columns $|\tilde i\rangle=V|i\rangle$ ), operators by matrices, and $O_R$ acts as $O_R\otimes I_{\overline R}$ . The code subspace is assumed nonzero (the lectures implicitly assume it: condition (4) requires $|R_3|<|S|$ and (4.18) normalizes by $|S|^{-1/2}$ ). In (4), $|R_2|=\lfloor|R|/|S|\rfloor$ and $|R_3|=|R|\bmod|S|$ are forced, and the statement is required for every identification of the basis of $\mathcal H_R$ with $(R_1\times R_2)\sqcup R_3$ ; $|\chi\rangle$ is required to be a unit vector.

Preamble

import Mathlib
import Definitions.Def_HarlowTASI_QuantumBasics

open Matrix
open scoped Kronecker

Formal statement

namespace HarlowTASI
theorem erasure_correction_tfae {R Rb C : Type} [Fintype R] [DecidableEq R] [Fintype Rb]
    [DecidableEq Rb] [Fintype C] [DecidableEq C] [Nonempty C]
    (V : Matrix (R × Rb) C ℂ) (hV : IsIsometry V) :
    List.TFAE
      [ ∀ O : Matrix C C ℂ, ∃ OR : Matrix R R ℂ,
          (OR ⊗ₖ (1 : Matrix Rb Rb ℂ)) * V = V * O ∧
          (ORᴴ ⊗ₖ (1 : Matrix Rb Rb ℂ)) * V = V * Oᴴ,
        ∀ X : Matrix Rb Rb ℂ, ∃ c : ℂ,
          (V * Vᴴ) * ((1 : Matrix R R ℂ) ⊗ₖ X) * (V * Vᴴ) = c • (V * Vᴴ),
        reducedSB (codeReferenceState V) =
          reducedS (codeReferenceState V) ⊗ₖ reducedB (codeReferenceState V),
        Fintype.card C ≤ Fintype.card R ∧
          ∀ e : R ≃ (C × Fin (Fintype.card R / Fintype.card C)) ⊕
              Fin (Fintype.card R % Fintype.card C),
            ∃ UR : Matrix R R ℂ, IsUnitaryMatrix UR ∧
              ∃ χ : Fin (Fintype.card R / Fintype.card C) × Rb → ℂ,
                ∑ x, ‖χ x‖ ^ 2 = 1 ∧
                ∀ (i : C) (r : R) (b : Rb),
                  V (r, b) i = ∑ r', UR r r' *
                    (match e r' with
                      | Sum.inl (c, k) => if c = i then χ (k, b) else 0
                      | Sum.inr _ => 0) ] := 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. 28–29, Theorem 4.1, eqs. (4.16)–(4.20).

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. Finite sets $R$ , $\overline R$ , $C$ with decidable equality, $C$ nonempty; a complex matrix $V$ with rows indexed by $R\times\overline R$ and columns by $C$ , assumed to be an isometry, $V^\dagger V=I_C$ .

Claim. The following four statements are pairwise equivalent:

For every $C\times C$ complex matrix $O$ there is an $R\times R$ matrix $O_R$ with

(O_R\otimes I_{\overline R})V=VO\quad\text{and}\quad(O_R^\dagger\otimes I_{\overline R})V=VO^\dagger .

For every $\overline R\times\overline R$ matrix $X$ there is $c\in\mathbb C$ with $(VV^\dagger)(I_R\otimes X)(VV^\dagger)=c\,(VV^\dagger)$ .
Let $\phi(s,r,b)=|C|^{-1/2}V_{(r,b),s}$ ( $s\in C$ , $r\in R$ , $b\in\overline R$ ). Then $\rho_{S\overline R}(\phi)=\rho_S(\phi)\otimes\rho_{\overline R}(\phi)$ as matrices indexed by $C\times\overline R$ , where $\rho_{S\overline R}((s,b),(s',b'))=\sum_r\phi(s,r,b)\overline{\phi(s',r,b')}$ , $\rho_S(s,s')=\sum_{r,b}\phi(s,r,b)\overline{\phi(s',r,b)}$ , $\rho_{\overline R}(b,b')=\sum_{s,r}\phi(s,r,b)\overline{\phi(s,r,b')}$ , and $\otimes$ is the Kronecker product.
$|C|\le|R|$ , and, writing $q=\lfloor |R|/|C|\rfloor$ and $m=|R|\bmod |C|$ : for every bijection $e:R\to(C\times\{0,..,q-1\})\sqcup\{0,..,m-1\}$ there exist an $R\times R$ matrix $U_R$ with $U_R^\dagger U_R=I$ and $U_RU_R^\dagger=I$ , and a function $\chi:\{0,..,q-1\}\times\overline R\to\mathbb C$ with $\sum_x|\chi(x)|^2=1$ , such that for all $i\in C$ , $r\in R$ , $b\in\overline R$ ,

V_{(r,b),i}=\sum_{r'\in R}(U_R)_{r,r'}\,F_i(r',b),\qquad F_i(r',b)=\begin{cases}\chi(k,b)&\text{if }e(r')=(c,k)\text{ in the first summand and }c=i,\\0&\text{if }e(r')=(c,k)\text{ with }c\neq i,\\0&\text{if }e(r')\text{ lies in the second summand.}\end{cases}

Edge remarks: because $C$ is nonempty, $|C|\ge1$ , so the division and remainder are ordinary. If no bijection $e$ exists the second half of (4) would be vacuous, but the cardinalities always match ( $|R|=|C|q+m$ ). The isometry hypothesis is the only assumption on $V$ .

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