Measured probabilities are linear in the state: $p_{\rm meas}=r\cdot p$

Proved

HardyFiveAxioms.measured_probability_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 $f:\mathbb R^K\to\mathbb R$ be a measured probability with $f(0)=0$ that respects mixtures on $S$ :

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

Then there is a vector $r\in\mathbb R^K$ such that

f(p)=r\cdot p=\sum_{k=1}^K r_kp^k\qquad\text{for all }p\in S .

This is Eq. (44) of the paper, proved in Appendix 1: every probability measurement is represented by a measurement vector $r$ .

Formalization Note The paper's Appendix 1 extends Eq. (112) beyond $S$ by fiat ("we are free to impose"). The present statement only asks for a linear representation on $S$ itself, which needs no such extension. The hypothesis $f(0)=0$ expresses that the null state never produces a non-null outcome.

Preamble

import Mathlib

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 6.6, Eq. (44) and Appendix 1: a measured probability `f(p)` that
respects mixtures on the convex set `S` of states (which contains the null state, on which
`f` vanishes) is given by a linear functional `p_meas = r · p`. -/
theorem measured_probability_linear {K : ℕ} (S : Set (Fin K → ℝ)) (hS : Convex ℝ S)
    (h0 : (0 : Fin K → ℝ) ∈ S) (f : (Fin K → ℝ) → ℝ) (hf0 : f 0 = 0)
    (hmix : ∀ pA ∈ S, ∀ pB ∈ S, ∀ t : ℝ, 0 ≤ t → t ≤ 1 →
      f (t • pA + (1 - t) • pB) = t * f pA + (1 - t) * f pB) :
    ∃ r : Fin K → ℝ, ∀ p ∈ S, f p = ∑ k, r k * p k := 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. 11, Section 6.6, Eqs. (41)–(44); pp. 28–29, Appendix 1, Eqs. (107)–(117)

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 a convex set containing the zero vector, and let $f:\mathbb R^K\to\mathbb R$ be any function with $f(0)=0$ . Assume that for all $p_A,p_B\in S$ and every real $t$ with $0\le t\le1$ ,

f(tp_A+(1-t)p_B)=t\,f(p_A)+(1-t)\,f(p_B).

Then there is a vector $r\in\mathbb R^K$ such that $f(p)=\sum_{k}r_k\,p_k$ for every $p\in S$ . Nothing is asserted about $f$ outside $S$ . No boundedness of $S$ , no range condition $0\le f\le1$ , and no spanning condition on $S$ are assumed.

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

Measured probabilities are linear in the state: pmeas=r⋅pp_{\rm meas}=r\cdot ppmeas​=r⋅p

Measured probabilities are linear in the state: $p_{\rm meas}=r\cdot p$