Theorem 20 — the normalized states of every system are the density matrices on $\mathbb C^{d_A}$

Open

InfoDerivQT.states_are_density_matrices

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

operational-probabilistic-theoriesquantum-foundationsquantum-information

Let $T$ be an operational-probabilistic theory satisfying causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning and purification, and let $A$ be a system. Then there are $n\in\mathbb N$ and a real-linear isomorphism $S$ from $\mathrm{St}_{\mathbb R}(A)$ onto the space of $n\times n$ complex Hermitian matrices such that

S\big(\mathrm{St}_1(A)\big)=\{M\in M_n(\mathbb C):\ M\succeq0,\ \operatorname{tr}M=1\},

and $n$ equals the size $N$ of every maximal set of perfectly distinguishable pure states of $A$ (the informational dimension $d_A$ ).

This is the paper's main result: the state space of every system is the set of density matrices on $\mathbb C^{d_A}$ .

Formalization Note The Hermitian matrices are Mathlib's selfAdjoint (Matrix (Fin n) (Fin n) ℂ) as a real vector space; positivity is Matrix.PosSemidef with the standard order on $\mathbb C$ .

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles
open scoped ComplexOrder

Formal statement

namespace InfoDerivQT
theorem states_are_density_matrices (T : OPT) (hT : T.SatisfiesPrinciples) (A : T.Sys) :
    ∃ (n : ℕ) (S : Vec (T.size A) ≃ₗ[ℝ] selfAdjoint (Matrix (Fin n) (Fin n) ℂ)),
      (fun ρ => (S ρ : Matrix (Fin n) (Fin n) ℂ)) '' T.St1 A =
        {M | M.PosSemidef ∧ M.trace = 1} ∧
      ∀ (N : ℕ) (φ : Fin N → Vec (T.size A)), T.IsMaximalPerfDistPure A φ → N = n := by sorry
end InfoDerivQT

Source

G. Chiribella, G. M. D'Ariano, P. Perinotti, *Informational derivation of quantum theory*, Phys. Rev. A 84, 012311 (2011), https://doi.org/10.1103/PhysRevA.84.012311 (arXiv:1011.6451), p. 012311-38, Sec. XIII, Theorem 20

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

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 paper and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; an independent, blind read-back should replace it before the proposal is relied upon.

Fix an operational-probabilistic theory $T$ (structure OPT, with all its framework axioms) satisfying all six principles (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning, purification as defined in the principles file), and a system $A$ . The conclusion is that there exist a natural number $n$ and a real-linear bijection $S$ from $\mathbb R^{D_A}$ onto the real vector space of complex $n\times n$ self-adjoint (Hermitian) matrices such that (i) the image under $S$ of the set of deterministic states of $A$ (vectors $\rho$ for which the one-element family $\{\rho\}$ is a preparation test) is exactly the set of complex $n\times n$ matrices that are positive semidefinite and have trace $1$ ; and (ii) for every natural number $N$ and every family $\varphi_0,\dots,\varphi_{N-1}$ that is a maximal perfectly distinguishable family of pure states of $A$ , $N=n$ . If $A$ has no deterministic states, (i) forces the image to be empty, which happens only for $n=0$ .

Human review

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

View graph

Theorem 20 — the normalized states of every system are the density matrices on CdA\mathbb C^{d_A}CdA​

Theorem 20 — the normalized states of every system are the density matrices on $\mathbb C^{d_A}$