Classical theory: no continuous path through pure states

Proved

HardyFiveAxioms.classical_no_continuous_pure_path

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

mathematical-physicsprobabilityquantum-foundationstopology

Let $N\in\mathbb N$ and let $\gamma:[0,1]\to\mathbb R^N$ be a continuous path such that $\gamma(t)$ is a pure state of the classical state space $S^{\rm cl}_N$ for every $t$ . Then $\gamma$ is constant:

\gamma(t)=\gamma(0)\qquad\text{for all }t\in[0,1].

Hence classical probability theory violates the continuity axiom: a continuous reversible transformation would move a pure state along a continuous path of pure states, which is impossible between two distinct basis states.

Formalization Note The path is a continuous map on unitInterval with the Euclidean (product) topology on $\mathbb R^N$ .

Preamble

import Mathlib
import Definitions.Def_hardy2001_states

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Sections 4 and 7: in classical probability theory there is no continuous
trajectory through the pure states connecting two different pure states: a continuous path
`[0,1] → ℝᴺ` that stays within the pure states is constant. -/
theorem classical_no_continuous_pure_path (N : ℕ) (γ : unitInterval → (Fin N → ℝ))
    (hγ : Continuous γ) (hpure : ∀ t, γ t ∈ pureStates (classicalStates N)) :
    ∀ t, γ t = γ 0 := 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. 5–6, Section 4, final paragraph; p. 15, Section 7, paragraph on classical systems

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.

Let $N\in\mathbb N$ and let $\gamma$ be a continuous map from the closed unit interval $[0,1]$ to $\mathbb R^N$ , with the usual topology. Assume that for every $t\in[0,1]$ , $\gamma(t)$ is a pure state of $S^{\rm cl}_N$ , i.e. a nonzero extreme point of $\{p\in\mathbb R^N: p\ge0,\ \sum_np_n\le1\}$ . Then $\gamma(t)=\gamma(0)$ for every $t\in[0,1]$ . For $N=0$ there are no pure states, so the hypothesis cannot hold and the statement is vacuous in that case only.

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