Reversible transformations send pure states to pure states

Proved

HardyFiveAxioms.reversible_maps_pure_to_pure

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 states and let $Z$ be an invertible real $K\times K$ matrix such that both $Z$ and $Z^{-1}$ map $S$ into itself (a reversible transformation). If $p$ is a pure state of $S$ , i.e. an extremal point of $S$ other than $0$ , then

Zp\in S_{\rm pure}.

Formalization Note " $Z^{-1}$ exists and is in $\Gamma$ " is encoded as invertibility of $Z$ together with $Z^{-1}S\subseteq S$ . Pure states are as in the definition file hardy2001_states.

Preamble

import Mathlib
import Definitions.Def_hardy2001_states

Formal statement

namespace HardyFiveAxioms

open Matrix

/-- Hardy 2001, Section 7: a reversible transformation (an invertible matrix `Z` such that both
`Z` and `Z⁻¹` map the state space `S` into itself) sends pure states to pure states. -/
theorem reversible_maps_pure_to_pure {K : ℕ} (S : Set (Fin K → ℝ))
    (Z : Matrix (Fin K) (Fin K) ℝ) (hZ : IsUnit Z)
    (hZS : ∀ p ∈ S, Z *ᵥ p ∈ S) (hZinvS : ∀ p ∈ S, Z⁻¹ *ᵥ p ∈ S)
    (p : Fin K → ℝ) (hp : p ∈ pureStates S) :
    Z *ᵥ p ∈ pureStates S := 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, p. 15, Section 7, paragraph 'If a reversible transformation is applied to a pure state it must necessarily output a pure state'

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 $K\in\mathbb N$ , let $S\subseteq\mathbb R^K$ be any set (no convexity assumed), and let $Z$ be a real $K\times K$ matrix that is invertible. Assume $Zp\in S$ for every $p\in S$ and $Z^{-1}p\in S$ for every $p\in S$ , where $Z^{-1}$ is the matrix inverse. Let $p\in\mathbb R^K$ be a pure state of $S$ : $p\in S$ , $p$ is an extreme point of $S$ , and $p\neq0$ . Then $Zp$ is also a pure state of $S$ : $Zp$ is an extreme point of $S$ and $Zp\neq0$ .

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