Theorem 12 — dimension of the state space, $D_A=d_A^2$

Open

InfoDerivQT.size_eq_dim_sq

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$ is a maximal set of perfectly distinguishable pure states of $A$ , then the dimension of the real vector space spanned by the states is

D_A=N^2=d_A^2.

This is the relation between the size of the state space and the number of perfectly distinguishable states that Hardy took as an axiom.

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles

Formal statement

namespace InfoDerivQT
theorem size_eq_dim_sq (T : OPT) (hT : T.SatisfiesPrinciples) (A : T.Sys)
    {N : ℕ} (φ : Fin N → Vec (T.size A)) (hφ : T.IsMaximalPerfDistPure A φ) :
    T.size A = N ^ 2 := 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-21, Sec. IX, Theorem 12 (Dimension of the state space)

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). The conclusion is that the size $D_A$ of $A$ — the number of real coordinates of its state space $\mathbb R^{D_A}$ , which by the framework axioms equals the dimension of the span of the states — equals $N^2$ .

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 12 — dimension of the state space, DA=dA2D_A=d_A^2DA​=dA2​

Theorem 12 — dimension of the state space, $D_A=d_A^2$