Theorem 9 (with Lemma 10) — the invariant state is $\chi_A=\frac1{d_A}\sum_i\varphi_i$

Open

InfoDerivQT.invariant_state_uniform_mixture

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_i\}_{i=1}^N$ a maximal set of perfectly distinguishable pure states. Put $\chi=\frac1N\sum_{i=1}^N\varphi_i$ . Then

$\mathcal U\chi=\chi$ for every reversible transformation $\mathcal U$ of $A$ ;
$\chi$ is the only normalized state of $A$ with this property.

Thus the unique invariant state $\chi_A$ of Lemma 10 equals $\frac1{d_A}\sum_i\varphi_i$ for every maximal set.

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles

Formal statement

namespace InfoDerivQT
theorem invariant_state_uniform_mixture (T : OPT) (hT : T.SatisfiesPrinciples) (A : T.Sys)
    {N : ℕ} (φ : Fin N → Vec (T.size A)) (hφ : T.IsMaximalPerfDistPure A φ) :
    (∀ U : Vec (T.size A) →ₗ[ℝ] Vec (T.size A), T.IsReversible A A U →
        U ((1 / (N : ℝ)) • ∑ i, φ i) = (1 / (N : ℝ)) • ∑ i, φ i) ∧
    ∀ ω ∈ T.St1 A, (∀ U : Vec (T.size A) →ₗ[ℝ] Vec (T.size A), T.IsReversible A A U →
        U ω = ω) → ω = (1 / (N : ℝ)) • ∑ 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 9; uniqueness of the invariant state: p. 012311-10, Lemma 10

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$ and a maximal perfectly distinguishable family of pure states $\varphi_0,\dots,\varphi_{N-1}$ of $A$ (deterministic members, an observation test with $a_j(\varphi_i)=\delta_{ij}$ , no deterministic state can be appended, all members pure). Let $\chi=\frac1N\sum_i\varphi_i$ (if $N=0$ this is the zero vector, since $1/0=0$ in this convention). The statement asserts two things: (1) for every linear map $\mathcal U$ of $\mathbb R^{D_A}$ that is a reversible transformation (it lies in some test from $A$ to $A$ and has a two-sided inverse that also lies in some test from $A$ to $A$ ), $\mathcal U\chi=\chi$ ; (2) every deterministic state $\omega$ of $A$ with $\mathcal U\omega=\omega$ for all reversible $\mathcal U$ equals $\chi$ .

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 9 (with Lemma 10) — the invariant state is χA=1dA∑iφi\chi_A=\frac1{d_A}\sum_i\varphi_iχA​=dA​1​∑i​φi​

Theorem 9 (with Lemma 10) — the invariant state is $\chi_A=\frac1{d_A}\sum_i\varphi_i$