State transformations are linear: $p\mapsto Zp$

Proved

HardyFiveAxioms.transformation_linear

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

convex-geometrylinear-algebramathematical-physicsquantum-foundations

Let $S\subseteq\mathbb R^K$ be a convex set of states containing the null state $0$ . Let $g:\mathbb R^K\to\mathbb R^K$ describe the effect of a transformation device, with $g(0)=0$ , such that $g$ respects mixtures on $S$ :

g\big(\lambda p_A+(1-\lambda)p_B\big)=\lambda g(p_A)+(1-\lambda)g(p_B)\qquad(p_A,p_B\in S,\ 0\le\lambda\le1).

Then there is a real $K\times K$ matrix $Z$ with

g(p)=Zp\qquad\text{for all }p\in S .

This is Eq. (46) of the paper.

Formalization Note The hypothesis $g(0)=0$ expresses that an absent system stays absent. As for measurements, only a representation on $S$ is required.

Preamble

import Mathlib

Formal statement

namespace HardyFiveAxioms

open Matrix

/-- Hardy 2001, Section 6.7, Eq. (46): a state transformation `p ↦ g(p)` that respects
mixtures on the convex set `S` of states (and sends the null state to the null state) acts on
`S` as a real `K × K` matrix: `g(p) = Z p`. -/
theorem transformation_linear {K : ℕ} (S : Set (Fin K → ℝ)) (hS : Convex ℝ S)
    (h0 : (0 : Fin K → ℝ) ∈ S) (g : (Fin K → ℝ) → (Fin K → ℝ)) (hg0 : g 0 = 0)
    (hmix : ∀ pA ∈ S, ∀ pB ∈ S, ∀ t : ℝ, 0 ≤ t → t ≤ 1 →
      g (t • pA + (1 - t) • pB) = t • g pA + (1 - t) • g pB) :
    ∃ Z : Matrix (Fin K) (Fin K) ℝ, ∀ p ∈ S, g p = Z *ᵥ p := 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. 11–12, Section 6.7, Eq. (46)

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 convex with $0\in S$ , and let $g:\mathbb R^K\to\mathbb R^K$ be any map with $g(0)=0$ . Assume that for all $p_A,p_B\in S$ and all real $t\in[0,1]$ , $g(tp_A+(1-t)p_B)=t\,g(p_A)+(1-t)\,g(p_B)$ , with vector operations taken coordinatewise. Then there is a real $K\times K$ matrix $Z$ such that $g(p)=Zp$ (matrix–vector product) for every $p\in S$ . It is not assumed that $g$ maps $S$ into $S$ , and nothing is asserted outside $S$ .

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

State transformations are linear: p↦Zpp\mapsto Zpp↦Zp

State transformations are linear: $p\mapsto Zp$