The six principles: Axioms 1–5 and the purification postulate

Definition

InfoDerivQT_principles

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

operational-probabilistic-theoriesquantum-foundationsquantum-information

The six principles of the paper, for an operational-probabilistic theory $T$ .

Causality (Axiom 1). For every preparation test $\{\rho_i\}$ and observation tests $\{a_j\}$ , $\{b_k\}$ of the same system, $\sum_j(a_j|\rho_i)=\sum_k(b_k|\rho_i)$ for every $i$ .
Perfect distinguishability (Axiom 2). Every normalized state that is not completely mixed is perfectly distinguishable from some other normalized state.
Ideal compression (Axiom 3). For every normalized state $\rho$ of $A$ there are a system $C$ with $D_C\le D_A$ , an encoding $\mathcal E\in\mathrm{Transf}(A,C)$ and a decoding $\mathcal D\in\mathrm{Transf}(C,A)$ with $\mathcal D\mathcal E\sigma=\sigma$ for all $\sigma\in F_\rho$ (lossless) and such that every normalized state of $C$ equals $\mathcal E\sigma$ for some $\sigma\in F_\rho$ (maximally efficient).
Local distinguishability (Axiom 4). If $\rho\neq\sigma$ are normalized states of $AB$ , there are effects $a$ of $A$ and $b$ of $B$ with $(a\otimes b|\rho)\neq(a\otimes b|\sigma)$ .
Pure conditioning (Axiom 5). If $\Psi$ is a pure normalized state of $AB$ and $\{a_i\}$ is an observation test on $A$ made of atomic effects, every induced state $(a_i|_A|\Psi)_{AB}$ of $B$ is pure; and symmetrically for atomic observation tests on $B$ .
Purification (Postulate 1). Every normalized state $\rho$ of $A$ has a purification: a pure normalized state $\Psi$ of some $AB$ whose marginal $(e|_B|\Psi)_{AB}$ under a deterministic effect $e$ of $B$ is $\rho$ . If $\Psi,\Psi'$ are purifications of the same $\rho$ with the same purifying system $B$ , then $\Psi'=(\mathcal I_A\otimes\mathcal U)\Psi$ for some reversible transformation $\mathcal U$ of $B$ .

SatisfiesPrinciples is the conjunction of the six.

Formalization Note The marginal in Postulate 1 is taken with any deterministic effect of $B$ ; under causality the deterministic effect is unique.

Definition code

import Mathlib
import Definitions.Def_InfoDerivQT_framework

namespace InfoDerivQT

namespace OPT

variable (T : OPT)

/-- Axiom 1 (Causality): the marginal probability `∑ⱼ (aⱼ|ρᵢ)` of a preparation outcome does
not depend on the choice of the observation test `{aⱼ}`. -/
def Causal : Prop :=
  ∀ (A : T.Sys) (X Y Z : Type) [Fintype X] [Fintype Y] [Fintype Z]
    (ρ : X → Vec (T.size A)) (a : Y → Module.Dual ℝ (Vec (T.size A)))
    (b : Z → Module.Dual ℝ (Vec (T.size A))),
    ρ ∈ T.PrepTest A X → a ∈ T.ObsTest A Y → b ∈ T.ObsTest A Z →
    ∀ i, ∑ j, a j (ρ i) = ∑ k, b k (ρ i)

/-- Axiom 2 (Perfect distinguishability): every normalized state that is not completely mixed
can be perfectly distinguished from some other normalized state. -/
def PerfectDistinguishabilityAxiom : Prop :=
  ∀ (A : T.Sys) (ρ : Vec (T.size A)), ρ ∈ T.St1 A → ¬ T.IsCompletelyMixed A ρ →
    ∃ σ ∈ T.St1 A, T.PerfectlyDistinguishable A ![ρ, σ]

/-- An ideal compression scheme for the normalized state `ρ` of `A` into the system `C`:
an encoding `E ∈ Transf(A,C)` and a decoding `D ∈ Transf(C,A)` with `D_C ≤ D_A`, which is
lossless (`D E σ = σ` for all `σ ∈ F_ρ`) and maximally efficient (every normalized state of
`C` is `E σ` for some `σ ∈ F_ρ`). -/
def IsIdealCompression (A C : T.Sys) (ρ : Vec (T.size A))
    (E : Vec (T.size A) →ₗ[ℝ] Vec (T.size C)) (D : Vec (T.size C) →ₗ[ℝ] Vec (T.size A)) :
    Prop :=
  E ∈ T.Transf A C ∧ D ∈ T.Transf C A ∧ T.size C ≤ T.size A ∧
    (∀ σ ∈ T.face A ρ, D (E σ) = σ) ∧
    (∀ τ ∈ T.St1 C, ∃ σ ∈ T.face A ρ, E σ = τ)

/-- Axiom 3 (Ideal compression): every normalized state admits an ideal compression scheme. -/
def IdealCompressionAxiom : Prop :=
  ∀ (A : T.Sys) (ρ : Vec (T.size A)), ρ ∈ T.St1 A →
    ∃ (C : T.Sys) (E : Vec (T.size A) →ₗ[ℝ] Vec (T.size C))
      (D : Vec (T.size C) →ₗ[ℝ] Vec (T.size A)), T.IsIdealCompression A C ρ E D

/-- Axiom 4 (Local distinguishability): two different normalized states of `AB` give
different probabilities for at least one product effect `a ⊗ b`. -/
def LocalDistinguishability : Prop :=
  ∀ (A B : T.Sys) (ρ σ : Vec (T.size (T.comp A B))), ρ ∈ T.St1 (T.comp A B) →
    σ ∈ T.St1 (T.comp A B) → ρ ≠ σ →
    ∃ a ∈ T.Eff A, ∃ b ∈ T.Eff B, T.tensorEff (A := A) (B := B) a b ρ ≠ T.tensorEff (A := A) (B := B) a b σ

/-- Axiom 5 (Pure conditioning): if `Ψ` is a pure normalized state of `AB` and `{aᵢ}` is an
atomic observation test on one side, then each induced state on the other side is pure. -/
def PureConditioning : Prop :=
  ∀ (A B : T.Sys) (Ψ : Vec (T.size (T.comp A B))) (X : Type) [Fintype X],
    Ψ ∈ T.St1 (T.comp A B) → T.IsPure (T.comp A B) Ψ →
    (∀ a : X → Module.Dual ℝ (Vec (T.size A)), a ∈ T.ObsTest A X →
      (∀ i, T.IsAtomicEff A (a i)) → ∀ i, T.IsPure B (T.condL (A := A) (B := B) (a i) Ψ)) ∧
    (∀ b : X → Module.Dual ℝ (Vec (T.size B)), b ∈ T.ObsTest B X →
      (∀ i, T.IsAtomicEff B (b i)) → ∀ i, T.IsPure A (T.condR (A := A) (B := B) (b i) Ψ))

/-- `Ψ ∈ St₁(AB)` is a purification of `ρ ∈ St₁(A)` (with purifying system `B`): `Ψ` is pure
and its marginal on `A`, obtained by applying a deterministic effect on `B`, is `ρ`. -/
def IsPurification (A B : T.Sys) (ρ : Vec (T.size A)) (Ψ : Vec (T.size (T.comp A B))) :
    Prop :=
  Ψ ∈ T.St1 (T.comp A B) ∧ T.IsPure (T.comp A B) Ψ ∧ ∃ e ∈ T.DetEff B, T.condR (A := A) (B := B) e Ψ = ρ

/-- Postulate 1 (Purification): every normalized state has a purification, and, for a fixed
purifying system `B`, any two purifications of the same state are connected by a reversible
transformation on `B`. -/
def Purification : Prop :=
  (∀ (A : T.Sys) (ρ : Vec (T.size A)), ρ ∈ T.St1 A →
    ∃ (B : T.Sys) (Ψ : Vec (T.size (T.comp A B))), T.IsPurification A B ρ Ψ) ∧
  (∀ (A B : T.Sys) (ρ : Vec (T.size A)) (Ψ Ψ' : Vec (T.size (T.comp A B))),
    T.IsPurification A B ρ Ψ → T.IsPurification A B ρ Ψ' →
    ∃ U : Vec (T.size B) →ₗ[ℝ] Vec (T.size B), T.IsReversible B B U ∧
      T.tensorT (A := A) (B := A) (A' := B) (B' := B) LinearMap.id U Ψ = Ψ')

/-- The six principles of the paper: Axioms 1–5 and Postulate 1. -/
structure SatisfiesPrinciples : Prop where
  causal : T.Causal
  perfectDistinguishability : T.PerfectDistinguishabilityAxiom
  idealCompression : T.IdealCompressionAxiom
  localDistinguishability : T.LocalDistinguishability
  pureConditioning : T.PureConditioning
  purification : T.Purification

end OPT

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), pp. 012311-7 to 012311-9, Sec. III: Axioms 1–5 and Postulate 1

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.

The file imports the framework and defines, for a theory $T$ (structure OPT), the following propositions.

Causal: for every system $A$ , finite types $X,Y,Z$ , preparation test $\{\rho_i\}_{i\in X}$ and observation tests $\{a_j\}_{j\in Y}$ , $\{b_k\}_{k\in Z}$ of $A$ , and every $i$ : $\sum_ja_j(\rho_i)=\sum_kb_k(\rho_i)$ .
PerfectDistinguishabilityAxiom: for every system $A$ and $\rho\in\mathrm{St}_1(A)$ that is not completely mixed, there is $\sigma\in\mathrm{St}_1(A)$ such that the two-element family $(\rho,\sigma)$ is perfectly distinguishable.
IsIdealCompression A C ρ E D (for systems $A,C$ , a vector $\rho$ , linear maps $E:\mathbb R^{D_A}\to\mathbb R^{D_C}$ , $D:\mathbb R^{D_C}\to\mathbb R^{D_A}$ ): $E\in\mathrm{Transf}(A,C)$ , $D\in\mathrm{Transf}(C,A)$ , $D_C\le D_A$ , $D(E\sigma)=\sigma$ for all $\sigma\in F_\rho$ , and every $\tau\in\mathrm{St}_1(C)$ equals $E\sigma$ for some $\sigma\in F_\rho$ . IdealCompressionAxiom: every $\rho\in\mathrm{St}_1(A)$ admits some system $C$ and maps $E,D$ with this property.
LocalDistinguishability: for all systems $A,B$ and $\rho,\sigma\in\mathrm{St}_1(AB)$ with $\rho\neq\sigma$ , there are $a\in\mathrm{Eff}(A)$ , $b\in\mathrm{Eff}(B)$ with $(a\otimes b)(\rho)\neq(a\otimes b)(\sigma)$ .
PureConditioning: for all systems $A,B$ , every $\Psi\in\mathrm{St}_1(AB)$ that is pure, and every finite type $X$ : (i) for every observation test $\{a_i\}_{i\in X}$ of $A$ all of whose members are atomic effects, each vector $\mathrm{condL}(a_i)\Psi$ is a pure state of $B$ ; (ii) for every observation test $\{b_i\}_{i\in X}$ of $B$ with atomic members, each $\mathrm{condR}(b_i)\Psi$ is a pure state of $A$ .
IsPurification A B ρ Ψ: $\Psi\in\mathrm{St}_1(AB)$ , $\Psi$ is pure, and $\mathrm{condR}(e)\Psi=\rho$ for some deterministic effect $e$ of $B$ . Purification: (i) for every system $A$ and $\rho\in\mathrm{St}_1(A)$ there are a system $B$ and $\Psi$ with IsPurification A B ρ Ψ; (ii) for all systems $A,B$ , every vector $\rho$ and every $\Psi,\Psi'$ that are both purifications of $\rho$ with purifying system $B$ , there is a linear map $U$ of $\mathbb R^{D_B}$ that is a reversible transformation from $B$ to $B$ with $(\mathrm{id}_A\otimes U)\Psi=\Psi'$ .

SatisfiesPrinciples is the structure (conjunction) of these six propositions: Causal, PerfectDistinguishabilityAxiom, IdealCompressionAxiom, LocalDistinguishability, PureConditioning, Purification.

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