Lemma 32 — all maximal sets of perfectly distinguishable pure states have the same size

Open

InfoDerivQT.maximal_sets_same_card

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. If $\{\varphi_i\}_{i=1}^N$ and $\{\psi_j\}_{j=1}^M$ are both maximal sets of perfectly distinguishable pure states of $A$ , then

N=M.

The common value is the informational dimension $d_A$ of the system.

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles

Formal statement

namespace InfoDerivQT
theorem maximal_sets_same_card (T : OPT) (hT : T.SatisfiesPrinciples) (A : T.Sys)
    {N M : ℕ} (φ : Fin N → Vec (T.size A)) (ψ : Fin M → Vec (T.size A))
    (hφ : T.IsMaximalPerfDistPure A φ) (hψ : T.IsMaximalPerfDistPure A ψ) :
    N = M := 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. VII, Lemma 32

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$ , natural numbers $N,M$ and families $\varphi:\{0,\dots,N-1\}\to\mathbb R^{D_A}$ , $\psi:\{0,\dots,M-1\}\to\mathbb R^{D_A}$ . Assume each family is a maximal perfectly distinguishable family of pure states: all members are deterministic states, there is an observation test indexed by the same set with $a_j(\varphi_i)=\delta_{ij}$ , no deterministic state can be appended keeping the family perfectly distinguishable, and every member is pure (all its refinements in preparation tests are nonnegative multiples of it). The conclusion is $N=M$ . Neither $N$ nor $M$ is required to be positive.

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