Theorem 8 — every pure state has a unique atomic effect with $(a|\varphi)=1$

Open

InfoDerivQT.pure_state_atomic_effect_duality

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, and $\varphi\in\mathrm{St}_1(A)$ a pure normalized state. Then there is exactly one atomic effect $a\in\mathrm{Eff}(A)$ such that

(a|\varphi)=1.

Together with Theorem 7 this establishes the duality between pure states and normalized atomic effects.

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles

Formal statement

namespace InfoDerivQT
theorem pure_state_atomic_effect_duality (T : OPT) (hT : T.SatisfiesPrinciples) (A : T.Sys)
    (φ : Vec (T.size A)) (hφ₁ : φ ∈ T.St1 A) (hφ : T.IsPure A φ) :
    ∃! a : Module.Dual ℝ (Vec (T.size A)), T.IsAtomicEff A a ∧ a φ = 1 := 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-16, Sec. VI, Theorem 8

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 vector $\varphi\in\mathbb R^{D_A}$ that is a deterministic state (the one-element family $\{\varphi\}$ is a preparation test) and pure (it belongs to some preparation test, and every refinement of it, i.e. every member $t_x$ , $x\in X_0$ , of a preparation test with $\varphi=\sum_{x\in X_0}t_x$ , equals $p\varphi$ with $p\ge0$ ). The statement asserts that there exists exactly one linear functional $a$ on $\mathbb R^{D_A}$ that is an atomic effect (it belongs to some observation test and all its refinements within observation tests are nonnegative multiples of it) and satisfies $a(\varphi)=1$ .

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 8 — every pure state has a unique atomic effect with (a∣φ)=1(a|\varphi)=1(a∣φ)=1

Theorem 8 — every pure state has a unique atomic effect with $(a|\varphi)=1$