Corollary 15 — informational dimension is multiplicative, $d_{AB}=d_Ad_B$

Open

InfoDerivQT.dim_composite

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

operational-probabilistic-theoriesquantum-foundationsquantum-information

Let $T$ satisfy the six principles and $A,B$ systems. If $A$ , $B$ and $AB$ have maximal sets of perfectly distinguishable pure states of sizes $N$ , $M$ and $K$ respectively, then

K=N\,M,

that is, $d_{AB}=d_A\,d_B$ .

Preamble

import Mathlib
import Definitions.Def_InfoDerivQT_principles

Formal statement

namespace InfoDerivQT
theorem dim_composite (T : OPT) (hT : T.SatisfiesPrinciples) (A B : T.Sys)
    {N M K : ℕ} (φ : Fin N → Vec (T.size A)) (ψ : Fin M → Vec (T.size B))
    (Φ : Fin K → Vec (T.size (T.comp A B)))
    (hφ : T.IsMaximalPerfDistPure A φ) (hψ : T.IsMaximalPerfDistPure B ψ)
    (hΦ : T.IsMaximalPerfDistPure (T.comp A B) Φ) :
    K = 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, Corollary 15

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, systems $A,B$ , natural numbers $N,M,K$ , and families $\varphi$ (indexed by $\{0,\dots,N-1\}$ , in $\mathbb R^{D_A}$ ), $\psi$ (indexed by $\{0,\dots,M-1\}$ , in $\mathbb R^{D_B}$ ) and $\Phi$ (indexed by $\{0,\dots,K-1\}$ , in $\mathbb R^{D_{AB}}$ ), each a maximal perfectly distinguishable family of pure states of its system (deterministic members, an observation test with $a_j(\cdot_i)=\delta_{ij}$ , no deterministic state can be appended, all members pure). The conclusion is $K=N\cdot M$ .

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

Corollary 15 — informational dimension is multiplicative, dAB=dAdBd_{AB}=d_Ad_BdAB​=dA​dB​

Corollary 15 — informational dimension is multiplicative, $d_{AB}=d_Ad_B$