Case $K=N$ : the solutions of $\sum_k(p^k)^2=1$ , $0\le p^k\le1$ , $\sum_kp^k=1$ are basis vectors

Proved

HardyFiveAxioms.k_eq_n_pure_vectors

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

inequalitiesmathematical-physicsquantum-foundations

Let $p=(p^1,\dots,p^N)\in\mathbb R^N$ satisfy

\sum_{k=1}^N(p^k)^2=1,\qquad 0\le p^k\le1\ \ (k=1,\dots,N),\qquad \sum_{k=1}^Np^k=1 .

Then one entry of $p$ equals $1$ and all others equal $0$ , i.e. $p=e_n$ for some $n$ .

In the case $K=N$ , Hardy shows that $D$ is the identity, so pure states satisfy Eq. (71), Eqs. (72)–(73) hold for normalized states, and the pure states are only the basis vectors. This is the step used to rule out $K=N$ by the continuity axiom.

Formalization Note Entries are indexed by Fin N.

Preamble

import Mathlib

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 8.5, Eqs. (71)–(73): the only solutions of `∑ₖ (pᵏ)² = 1`,
`0 ≤ pᵏ ≤ 1`, `∑ₖ pᵏ = 1` are the basis vectors (one entry `1`, all others `0`). -/
theorem k_eq_n_pure_vectors (N : ℕ) (p : Fin N → ℝ)
    (hsq : ∑ k, p k ^ 2 = 1) (hbd : ∀ k, 0 ≤ p k ∧ p k ≤ 1) (hnorm : ∑ k, p k = 1) :
    ∃ n : Fin N, p = Pi.single n 1 := 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. 19–20, Section 8.5, Eqs. (70)–(73)

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 $p\in\mathbb R^N$ with $\sum_k p_k^2=1$ , with $0\le p_k$ and $p_k\le1$ for every $k$ , and with $\sum_kp_k=1$ . Then there is an index $n\in\{0,\dots,N-1\}$ such that $p$ equals the vector with $1$ at position $n$ and $0$ elsewhere. For $N=0$ the hypotheses are contradictory, because the sums are $0$ .

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

Case K=NK=NK=N: the solutions of ∑k(pk)2=1\sum_k(p^k)^2=1∑k​(pk)2=1, 0≤pk≤10\le p^k\le10≤pk≤1, ∑kpk=1\sum_kp^k=1∑k​pk=1 are basis vectors

Case $K=N$ : the solutions of $\sum_k(p^k)^2=1$ , $0\le p^k\le1$ , $\sum_kp^k=1$ are basis vectors