Theorem 10 — spectral decomposition into perfectly distinguishable pure states

Open

InfoDerivQT.spectral_decomposition

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

operational-probabilistic-theoriesquantum-foundationsquantum-information

Let $T$ satisfy the six principles and $A$ a system. Every normalized state $\rho\in\mathrm{St}_1(A)$ can be written as

\rho=\sum_{i=1}^N p_i\,\varphi_i,\qquad p_i\ge0,\quad \sum_i p_i=1,

where $\varphi_1,\dots,\varphi_N$ are perfectly distinguishable pure states.

This is the operational counterpart of the spectral theorem for density matrices.

Formalization Note The paper states the result for mixed states; for pure states it holds trivially with $N=1$ , so the formal statement covers all normalized states.

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles

Formal statement

namespace InfoDerivQT
theorem spectral_decomposition (T : OPT) (hT : T.SatisfiesPrinciples) (A : T.Sys)
    (ρ : Vec (T.size A)) (hρ : ρ ∈ T.St1 A) :
    ∃ (N : ℕ) (φ : Fin N → Vec (T.size A)) (p : Fin N → ℝ),
      T.PerfectlyDistinguishable A φ ∧ (∀ i, T.IsPure A (φ i)) ∧
      (∀ i, 0 ≤ p i) ∧ ∑ i, p i = 1 ∧ ρ = ∑ i, p i • φ i := 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-17, Sec. VIII, Theorem 10 (Spectral decomposition)

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 $T$ satisfying all six principles, a system $A$ , and a deterministic state $\rho$ of $A$ (the one-element family $\{\rho\}$ is a preparation test). The conclusion is that there exist a natural number $N$ , a family $\varphi_0,\dots,\varphi_{N-1}$ in $\mathbb R^{D_A}$ and real numbers $p_0,\dots,p_{N-1}$ such that: the family $\varphi$ is perfectly distinguishable (all members deterministic states, and some observation test $\{a_j\}_{j<N}$ has $a_j(\varphi_i)=\delta_{ij}$ ); every $\varphi_i$ is pure (it belongs to some preparation test and all its refinements are nonnegative multiples of it); every $p_i\ge0$ ; $\sum_ip_i=1$ ; and $\rho=\sum_ip_i\varphi_i$ . Pure $\rho$ are not excluded.

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