Theorem 6 — a perfectly distinguishable set is maximal iff its uniform mixture is completely mixed

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 an operational-probabilistic theory $T$ (structure OPT) that satisfies all six principles, a system $A$, a natural number $N$ with $N>0$, and a family $\rho:\{0,\dots,N-1\}\to\mathbb R^{D_A}$ that is perfectly distinguishable, meaning: every $\rho_i$ is a deterministic state (the one-element family $\{\rho_i\}$ is a preparation test) and some observation test $\{a_j\}_{j<N}$ satisfies $a_j(\rho_i)=1$ if $i=j$ and $0$ otherwise. The statement asserts the equivalence of: (1) the family is maximal, i.e. it is perfectly distinguishable and for every deterministic state $\sigma$ the extended family $(\rho_0,\dots,\rho_{N-1},\sigma)$ is not perfectly distinguishable; (2) the vector $\omega=\frac1N\sum_i\rho_i$ is completely mixed, i.e. $\omega$ is a state (belongs to some preparation test) and for every state $\tau$ there is $p>0$ such that $p\tau$ is a refinement of $\omega$ (there are a preparation test $\{t_x\}$ and a finite subset $X_0$ of outcomes with $\omega=\sum_{x\in X_0}t_x$ and $t_x=p\tau$ for some $x\in X_0$). The case $N=0$ is excluded by hypothesis.