Theorem 5.1 — every finite-dimensional von Neumann algebra is a block-diagonal direct sum of factors

Proved

HarlowTASI.vonNeumann_block_decomposition

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

holographyoperator-algebrasquantum-error-correctionquantum-information

Let $M$ be a von Neumann algebra on a finite-dimensional Hilbert space $\mathcal H$ , i.e. a set of operators closed under sums, products and adjoints and containing every $\lambda I$ (Definition 5.3). Then there is a Hilbert space direct sum decomposition

\mathcal H=\bigoplus_\alpha\big(\mathcal H_{r_\alpha}\otimes\mathcal H_{\overline r_\alpha}\big)\tag{5.12}

such that

M=\bigoplus_\alpha\big(\mathcal L(\mathcal H_{r_\alpha})\otimes I_{\overline r_\alpha}\big),\qquad M'=\bigoplus_\alpha\big(I_{r_\alpha}\otimes\mathcal L(\mathcal H_{\overline r_\alpha})\big),\qquad Z_M=\bigoplus_\alpha\lambda_\alpha I_{r_\alpha\overline r_\alpha},\tag{5.13}

where $M'$ is the commutant (Definition 5.4) and $Z_M=M\cap M'$ the center (Definition 5.5).

This structure theorem is what makes the algebraic entropy (5.16) and relative entropy (5.18) meaningful for an arbitrary von Neumann algebra, and it is the setting of Theorem 5.2.

Formalization Note $\mathcal H=\mathbb C^{C}$ , $M$ is a $*$ -subalgebra of the $C\times C$ complex matrices, the commutant is the centralizer, and the decomposition is a unitary $U:\mathbb C^C\to\bigoplus_{\alpha<N}\mathbb C^{d_{r_\alpha}}\otimes\mathbb C^{d_{\overline r_\alpha}}$ with all block dimensions positive.

Preamble

import Mathlib
import Definitions.Def_HarlowTASI_OperatorAlgebras

Formal statement

namespace HarlowTASI
theorem vonNeumann_block_decomposition {C : Type} [Fintype C] [DecidableEq C]
    (M : StarSubalgebra ℂ (Matrix C C ℂ)) :
    ∃ (N : ℕ) (dr drb : Fin N → ℕ) (U : Matrix (BlockIndex N dr drb) C ℂ),
      IsUnitaryMatrix U ∧ (∀ a, 0 < dr a ∧ 0 < drb a) ∧
      (M : Set (Matrix C C ℂ)) = blockAlgebraLeft U ∧
      (StarSubalgebra.centralizer ℂ (M : Set (Matrix C C ℂ)) : Set (Matrix C C ℂ)) =
        blockAlgebraRight U ∧
      ((M ⊓ StarSubalgebra.centralizer ℂ (M : Set (Matrix C C ℂ)) :
          StarSubalgebra ℂ (Matrix C C ℂ)) : Set (Matrix C C ℂ)) = blockAlgebraCenter 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, p. 44, Definitions 5.3–5.5 and Theorem 5.1, eqs. (5.12)–(5.13).

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. A finite set $C$ with decidable equality and a $*$ -subalgebra $M$ of the algebra of $C\times C$ complex matrices over $\mathbb C$ (closed under sums, products, scalar multiples and conjugate transpose, and containing the identity hence all $\lambda I$ ).

Claim. There exist $N\in\mathbb N$ , functions $d_r,d_{\overline r}:\{0,..,N-1\}\to\mathbb N$ , and a matrix $U$ with rows indexed by the block index set $\{(\alpha,i,j):\alpha<N,\ i<d_r(\alpha),\ j<d_{\overline r}(\alpha)\}$ and columns indexed by $C$ , such that

$U$ is unitary: $U^\dagger U=I$ and $UU^\dagger=I$ ;
$d_r(\alpha)\ge1$ and $d_{\overline r}(\alpha)\ge1$ for every $\alpha$ ;
$M$ (as a set) equals $\{U^\dagger\big(\bigoplus_\alpha x_\alpha\otimes I_{d_{\overline r}(\alpha)}\big)U\ :\ x_\alpha\text{ arbitrary } d_r(\alpha)\times d_r(\alpha)\text{ matrices}\}$ ;
the commutant $M'=\{Y: YX=XY\ \forall X\in M\}$ equals $\{U^\dagger\big(\bigoplus_\alpha I_{d_r(\alpha)}\otimes y_\alpha\big)U\ :\ y_\alpha\text{ arbitrary}\}$ ;
the center $M\cap M'$ equals $\{U^\dagger\big(\bigoplus_\alpha c_\alpha I\big)U\ :\ c_\alpha\in\mathbb C\}$ .

Edge remarks: if $C$ is empty, $N=0$ is allowed (empty direct sum). The block-diagonal matrices are zero off the diagonal blocks.

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