Theorem 5.2 — entanglement wedge reconstruction ⇔ quantum RT formula ⇔ JLMS formula

Proved

HarlowTASI.entanglement_wedge_reconstruction

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 a finite-dimensional Hilbert space, let $\mathcal H_{code}\subseteq\mathcal H$ be a subspace, and let $M$ be a von Neumann algebra on $\mathcal H_{code}$ with commutant $M'$ and center $Z_M$ . For a state $\tilde\rho$ on $\mathcal H_{code}$ write $\tilde\rho_R,\tilde\rho_{\overline R}$ for its reductions to $R$ and $\overline R$ , and $S(\tilde\rho,M)$ , $S(\tilde\rho|\tilde\sigma,M)$ for the algebraic entropy (5.16) and relative entropy (5.18). Then the following three statements are equivalent:

Subregion duality. For all $\tilde O\in M$ and $\tilde O'\in M'$ there are $O_R\in\mathcal L(\mathcal H_R)$ and $O'_{\overline R}\in\mathcal L(\mathcal H_{\overline R})$ such that for all $|\tilde\psi\rangle\in\mathcal H_{code}$

O_R|\tilde\psi\rangle=\tilde O|\tilde\psi\rangle,\quad O_R^\dagger|\tilde\psi\rangle=\tilde O^\dagger|\tilde\psi\rangle,\quad O'_{\overline R}|\tilde\psi\rangle=\tilde O'|\tilde\psi\rangle,\quad O'^\dagger_{\overline R}|\tilde\psi\rangle=\tilde O'^\dagger|\tilde\psi\rangle.\tag{5.19}

Quantum RT formula. There is an operator $\mathcal L_R\in Z_M$ such that for every state $\tilde\rho$ on $\mathcal H_{code}$

S(\tilde\rho_R)=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M),\qquad S(\tilde\rho_{\overline R})=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M').\tag{5.20}

JLMS formula. For all states $\tilde\rho,\tilde\sigma$ on $\mathcal H_{code}$

S(\tilde\rho_R|\tilde\sigma_R)=S(\tilde\rho|\tilde\sigma,M),\qquad S(\tilde\rho_{\overline R}|\tilde\sigma_{\overline R})=S(\tilde\rho|\tilde\sigma,M').\tag{5.21}

The theorem (proved in Harlow, The Ryu–Takayanagi formula from quantum error correction, 2017) shows that subregion duality in the entanglement wedge, the quantum Ryu–Takayanagi formula with a central area operator, and the JLMS formula are mathematically equivalent; the lectures name it as their main target. It does not assert that any of the three statements holds.

Formalization Note $\mathcal H_{code}$ is the image of an isometry $V:\mathbb C^C\to\mathbb C^{R\times\overline R}$ , states on it are $C\times C$ density matrices $\tilde\rho$ (embedded as $V\tilde\rho V^\dagger$ ), and $O_R$ acts as $O_R\otimes I_{\overline R}$ . $M$ is a $*$ -subalgebra of $C\times C$ matrices; the algebraic entropies are evaluated in an arbitrary block decomposition $U$ of $M$ (Theorem 5.1 guarantees one exists; the entropies do not depend on the choice). The RT identity is stated in $\mathbb C$ , so it also forces $\mathrm{Tr}(\tilde\rho\mathcal L_R)$ to be real; relative entropies are compared in the extended reals, so the value $+\infty$ is allowed on both sides.

Preamble

import Mathlib
import Definitions.Def_HarlowTASI_OperatorAlgebras

open Matrix
open scoped Kronecker

Formal statement

namespace HarlowTASI
theorem entanglement_wedge_reconstruction {R Rb C : Type} [Fintype R] [DecidableEq R]
    [Fintype Rb] [DecidableEq Rb] [Fintype C] [DecidableEq C]
    (V : Matrix (R × Rb) C ℂ) (hV : IsIsometry V)
    (M : StarSubalgebra ℂ (Matrix C C ℂ))
    (N : ℕ) (dr drb : Fin N → ℕ) (U : Matrix (BlockIndex N dr drb) C ℂ)
    (hU : IsUnitaryMatrix U) (hMU : (M : Set (Matrix C C ℂ)) = blockAlgebraLeft U) :
    List.TFAE
      [ ∀ O ∈ M, ∀ O' ∈ StarSubalgebra.centralizer ℂ (M : Set (Matrix C C ℂ)),
          ∃ (OR : Matrix R R ℂ) (ORb : Matrix Rb Rb ℂ),
            (OR ⊗ₖ (1 : Matrix Rb Rb ℂ)) * V = V * O ∧
            (ORᴴ ⊗ₖ (1 : Matrix Rb Rb ℂ)) * V = V * Oᴴ ∧
            ((1 : Matrix R R ℂ) ⊗ₖ ORb) * V = V * O' ∧
            ((1 : Matrix R R ℂ) ⊗ₖ ORbᴴ) * V = V * O'ᴴ,
        ∃ L ∈ M ⊓ StarSubalgebra.centralizer ℂ (M : Set (Matrix C C ℂ)),
          ∀ ρ : Matrix C C ℂ, IsDensityMatrix ρ →
            ((vonNeumannEntropy (traceRight (V * ρ * Vᴴ)) : ℝ) : ℂ) =
                (ρ * L).trace + ((algebraicEntropyLeft U ρ : ℝ) : ℂ) ∧
            ((vonNeumannEntropy (traceLeft (V * ρ * Vᴴ)) : ℝ) : ℂ) =
                (ρ * L).trace + ((algebraicEntropyRight U ρ : ℝ) : ℂ),
        ∀ ρ σ : Matrix C C ℂ, IsDensityMatrix ρ → IsDensityMatrix σ →
          relativeEntropy (traceRight (V * ρ * Vᴴ)) (traceRight (V * σ * Vᴴ)) =
              algebraicRelEntropyLeft U ρ σ ∧
          relativeEntropy (traceLeft (V * ρ * Vᴴ)) (traceLeft (V * σ * Vᴴ)) =
              algebraicRelEntropyRight U ρ σ ] := 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, §5.3, pp. 45–46, Theorem 5.2, eqs. (5.19)–(5.21), with the entropies of eqs. (5.14)–(5.18).

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$ (decidable equality); no nonemptiness is assumed.
A matrix $V$ (rows $R\times\overline R$ , columns $C$ ) with $V^\dagger V=I_C$ .
A $*$ -subalgebra $M$ of the $C\times C$ complex matrices (containing all $\lambda I$ ); $M'$ denotes its centralizer $\{Y:YX=XY\ \forall X\in M\}$ and $Z_M=M\cap M'$ .
$N\in\mathbb N$ , $d_r,d_{\overline r}:\{0,..,N-1\}\to\mathbb N$ (zero dimensions allowed), and a matrix $U$ (rows: block index set $\{(\alpha,i,j)\}$ , columns: $C$ ) with $U^\dagger U=I$ and $UU^\dagger=I$ .
Hypothesis: $M$ equals, as a set, $\{U^\dagger(\bigoplus_\alpha x_\alpha\otimes I_{d_{\overline r}(\alpha)})U\}$ over all families of $d_r(\alpha)\times d_r(\alpha)$ matrices $x_\alpha$ .

Notation: for a $C\times C$ matrix $\rho$ , $\rho_R=\mathrm{Tr}_{\overline R}(V\rho V^\dagger)$ and $\rho_{\overline R}=\mathrm{Tr}_R(V\rho V^\dagger)$ . $S_L,S_R$ and $S_L(\cdot|\cdot),S_R(\cdot|\cdot)$ are the block-wise algebraic entropies of the operator-algebra definition file, computed with this $U$ : $S_L(\rho)=-\sum_\alpha p_\alpha\log p_\alpha+\sum_\alpha p_\alpha S(\rho_{r_\alpha})$ with $p_\alpha$ the trace of the $\alpha$ -th diagonal block of $U\rho U^\dagger$ and $\rho_{r_\alpha}$ the normalized partial trace of that block over its second factor; $S_R$ uses the partial trace over the first factor; the relative versions add the classical term $c(p_\alpha(\rho),p_\alpha(\sigma))$ and $p_\alpha(\rho)\,S(\rho_{r_\alpha}|\sigma_{r_\alpha})$ (resp. $\overline r_\alpha$ ).

Claim. The following three statements are pairwise equivalent:

For every $O\in M$ and every $O'\in M'$ there exist an $R\times R$ matrix $O_R$ and an $\overline R\times\overline R$ matrix $O'_{\overline R}$ with

(O_R\otimes I)V=VO,\quad(O_R^\dagger\otimes I)V=VO^\dagger,\quad(I\otimes O'_{\overline R})V=VO',\quad(I\otimes O'^\dagger_{\overline R})V=VO'^\dagger .

There exists $L\in M\cap M'$ such that for every $C\times C$ density matrix $\rho$ (positive semidefinite, trace $1$ ), as complex numbers,

S(\rho_R)=\mathrm{Tr}(\rho L)+S_L(\rho)\quad\text{and}\quad S(\rho_{\overline R})=\mathrm{Tr}(\rho L)+S_R(\rho),

where $S(\cdot)$ is the von Neumann entropy (eigenvalue formula). 3. For all $C\times C$ density matrices $\rho,\sigma$ , as extended reals,

S(\rho_R|\sigma_R)=S_L(\rho|\sigma)\quad\text{and}\quad S(\rho_{\overline R}|\sigma_{\overline R})=S_R(\rho|\sigma),

where $S(\cdot|\cdot)$ is the spectral relative entropy (with value $+\infty$ when a nonzero eigenvalue direction of the first argument overlaps a zero eigenvalue direction of the second).

Edge remarks: if $C$ is empty there are no density matrices, so (2) and (3) hold trivially and (1) holds trivially as well. The theorem asserts only the equivalence, not that any of the statements is true.

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