Theorem 16 — superposition principle: every probability vector is realized by a pure state

Open

InfoDerivQT.superposition_principle

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

operational-probabilistic-theoriesquantum-foundationsquantum-information

Let $T$ satisfy the six principles, $A$ a system, $\{\varphi_i\}_{i=1}^N$ a maximal set of perfectly distinguishable pure states, and $\{a_i\}_{i=1}^N$ an observation test with $(a_i|\varphi_j)=\delta_{ij}$ . Then for every probability vector $(p_1,\dots,p_N)$ , $p_i\ge0$ , $\sum_ip_i=1$ , there is a pure state $\varphi_p\in\mathrm{St}_1(A)$ with

(a_i|\varphi_p)=p_i\qquad(i=1,\dots,N).

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles

Formal statement

namespace InfoDerivQT
theorem superposition_principle (T : OPT) (hT : T.SatisfiesPrinciples) (A : T.Sys)
    {N : ℕ} (φ : Fin N → Vec (T.size A)) (hφ : T.IsMaximalPerfDistPure A φ)
    (a : Fin N → Module.Dual ℝ (Vec (T.size A))) (ha : a ∈ T.ObsTest A (Fin N))
    (haφ : ∀ i j, a i (φ j) = if i = j then 1 else 0)
    (p : Fin N → ℝ) (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i = 1) :
    ∃ ψ ∈ T.St1 A, T.IsPure A ψ ∧ ∀ i, a i ψ = p 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-29, Sec. XII, Theorem 16 (Superposition principle for general systems)

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$ , a natural number $N$ , a maximal perfectly distinguishable family of pure states $\varphi_0,\dots,\varphi_{N-1}$ of $A$ , a family of linear functionals $a_0,\dots,a_{N-1}$ that is an observation test of $A$ (indexed by $\{0,\dots,N-1\}$ ) with $a_i(\varphi_j)=1$ if $i=j$ and $0$ otherwise, and real numbers $p_0,\dots,p_{N-1}$ with $p_i\ge0$ and $\sum_ip_i=1$ . The conclusion is that there exists $\psi\in\mathbb R^{D_A}$ which is a deterministic state, is pure (belongs to some preparation test, all refinements nonnegative multiples of it), and satisfies $a_i(\psi)=p_i$ for every $i$ .

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