Pure states, classical basis states and the classical state space

Definition

hardy2001_states

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

convex-geometrymathematical-physicsquantum-foundations

Let $S\subseteq\mathbb R^K$ be a set of (unnormalized) state vectors. Its set of pure states is

S_{\rm pure}=\operatorname{ext}(S)\setminus\{0\},

the extremal points of $S$ other than the null state $0$ . A point is extremal if it is not a proper convex combination of two other points of $S$ .

For a dimension $N$ , the basis states of classical probability theory are the unit vectors $e_n\in\mathbb R^N$ , with a $1$ in position $n$ and $0$ elsewhere. The classical state space is

S^{\rm cl}_N=\Big\{p\in\mathbb R^N:\ p_n\ge0\ \text{for all }n,\ \ \sum_{n}p_n\le1\Big\}.

This is the convex hull of the basis states and the null state.

These are the objects of Sections 4 and 6.9 of the paper: pure states are the definite states of a system, and the classical state space is a polytope.

Formalization Note Extremal points are Mathlib's Set.extremePoints ℝ S. Basis states are indexed by Fin N, so the paper's state $n$ is index $n-1$ .

Definition code

import Mathlib

namespace HardyFiveAxioms

/-- The pure states of a set `S` of (unnormalized) state vectors `p ∈ ℝᴷ`: the extremal points
of `S` other than the null state `0` (Hardy 2001, Section 6.9). -/
def pureStates {K : ℕ} (S : Set (Fin K → ℝ)) : Set (Fin K → ℝ) :=
  Set.extremePoints ℝ S \ {0}

/-- The `n`-th basis state of classical probability theory in dimension `N`: the vector with a
`1` in position `n` and `0` elsewhere (Hardy 2001, Eq. (2)). -/
def basisState {N : ℕ} (n : Fin N) : Fin N → ℝ :=
  Pi.single n 1

/-- The state space of classical probability theory in dimension `N` (Hardy 2001, Section 4):
the convex hull of the `N` basis states and the null state, i.e. the vectors `p ∈ ℝᴺ` with
nonnegative entries whose sum (the normalization coefficient) is at most `1`. -/
def classicalStates (N : ℕ) : Set (Fin N → ℝ) :=
  {p | (∀ n, 0 ≤ p n) ∧ ∑ n, p n ≤ 1}

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, Eq. (2) and the sentence defining pure states; p. 12, Section 6.9

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.

Three objects are defined.

For a natural number $K$ and a set $S$ of real vectors $p\in\mathbb R^K$ (functions from $\{0,\dots,K-1\}$ to $\mathbb R$ ), $\mathrm{pure}(S)$ is the set of points $p\in S$ that are extreme points of $S$ and are different from the zero vector. Here $p\in S$ is an extreme point when, whenever $p$ lies in the open segment between two points $x,y\in S$ , one has $x=p$ and $y=p$ . No convexity, boundedness or closedness of $S$ is assumed. If $S$ is empty, or $S=\{0\}$ , the set of pure states is empty.
For $N\in\mathbb N$ and an index $n\in\{0,\dots,N-1\}$ , $e_n\in\mathbb R^N$ is the vector with $1$ in coordinate $n$ and $0$ in every other coordinate.
For $N\in\mathbb N$ , $S^{\rm cl}_N$ is the set of $p\in\mathbb R^N$ with $p_n\ge0$ for every $n$ and $\sum_{n=0}^{N-1}p_n\le1$ . For $N=0$ it consists of the single (empty) vector.

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