Prove2Me

Classical pure states are exactly the NN basis states

Proved
HardyFiveAxioms.classical_pureStates_eq_basis

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

convex-geometrymathematical-physicsprobabilityquantum-foundations

For every dimension NN, the pure states of the classical state space SNcl={p∈RN:p≥0, ∑npn≤1}S^{\rm cl}_N=\{p\in\mathbb R^N: p\ge0,\ \sum_np_n\le1\} are exactly the NN basis states:

SN,purecl={e1,…,eN}.S^{\rm cl}_{N,\rm pure}=\{e_1,\dots,e_N\}.

This is the description of classical probability theory in Section 4 (Eq. (2)): the extremal states are the basis states and the null state, and the pure states are the basis states. In particular there are only finitely many pure states.

Formalization Note Pure states, basis states and SNclS^{\rm cl}_N are as in hardy2001_states.

Preamble
import Mathlib
import Definitions.Def_hardy2001_states
Formal statement
namespace HardyFiveAxioms

/-- Hardy 2001, Section 4, Eq. (2): the pure states of classical probability theory in
dimension `N` are exactly the `N` basis states. -/
theorem classical_pureStates_eq_basis (N : ℕ) :
    pureStates (classicalStates N) = Set.range (basisState (N := N)) := by sorry

end HardyFiveAxioms
Source
L. Hardy, *Quantum Theory From Five Reasonable Axioms*, arXiv:quant-ph/0101012v4 (2001), https://arxiv.org/abs/quant-ph/0101012, pp. 4–5, Section 4, Eqs. (1)–(3) and the definition of pure states
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 statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

For every natural number NN, the set of pure states of SNclS^{\rm cl}_N equals the set {e0,…,eN−1}\{e_0,\dots,e_{N-1}\} of standard unit vectors of RN\mathbb R^N. Here SNcl={p∈RN: pn≥0 ∀n, ∑npn≤1}S^{\rm cl}_N=\{p\in\mathbb R^N:\ p_n\ge0\ \forall n,\ \sum_n p_n\le1\}, and a pure state is an extreme point of that set that is not the zero vector. For N=0N=0 both sides are empty.

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