Hardy's $N^2$ fiducial projectors $|n\rangle\langle n|$ , $|mn\rangle_x\langle mn|$ , $|mn\rangle_y\langle mn|$

Definition

hardy2001_projectors

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

Let $|1\rangle,\dots,|N\rangle$ be the standard orthonormal basis of $\mathbb C^N$ . For $m<n$ put

|mn\rangle_x=\frac1{\sqrt2}\big(|m\rangle+|n\rangle\big),\qquad |mn\rangle_y=\frac1{\sqrt2}\big(|m\rangle+i|n\rangle\big).

For a vector $v\in\mathbb C^N$ , $|v\rangle\langle v|$ denotes the $N\times N$ matrix with entries $v_j\overline{v_k}$ . Hardy's fiducial projectors are the operators

|n\rangle\langle n|\ \ (1\le n\le N),\qquad |mn\rangle_x\langle mn|,\ \ |mn\rangle_y\langle mn|\ \ (1\le m<n\le N),

which number $N+2\binom N2=N^2$ in total. They are indexed by the disjoint union of $\{1,\dots,N\}$ with two copies of the set of pairs $m<n$ .

Section 5 uses these projectors to put quantum theory in a form resembling classical probability theory: the state is the vector of the $N^2$ probabilities $p_k=\mathrm{tr}(\hat P_k\hat\rho)$ .

Formalization Note Indices are Fin N, so $|n\rangle$ is ket (n-1). The two copies of the pairs are labelled false ( $x$ ) and true ( $y$ ). The paper writes $|mn\rangle_x\langle mn|$ for the projector onto $|mn\rangle_x$ , and similarly for $y$ . ket, ketX, ketY and proj are also used directly in other statements of this mission.

Definition code

import Mathlib

namespace HardyFiveAxioms

/-- The orthonormal basis vector `|n⟩ ∈ ℂᴺ`. -/
def ket {N : ℕ} (n : Fin N) : Fin N → ℂ :=
  Pi.single n 1

/-- `|mn⟩ₓ = (|m⟩ + |n⟩)/√2` (Hardy 2001, Section 5). -/
noncomputable def ketX {N : ℕ} (m n : Fin N) : Fin N → ℂ :=
  ((1 / Real.sqrt 2 : ℝ) : ℂ) • (ket m + ket n)

/-- `|mn⟩_y = (|m⟩ + i|n⟩)/√2` (Hardy 2001, Section 5). -/
noncomputable def ketY {N : ℕ} (m n : Fin N) : Fin N → ℂ :=
  ((1 / Real.sqrt 2 : ℝ) : ℂ) • (ket m + Complex.I • ket n)

/-- The operator `|v⟩⟨v|` on `ℂᴺ`, as the matrix with entries `vᵢ · conj(vⱼ)`. -/
def proj {N : ℕ} (v : Fin N → ℂ) : Matrix (Fin N) (Fin N) ℂ :=
  Matrix.vecMulVec v (star v)

/-- Index set of Hardy's `N²` fiducial projectors: one for each basis vector `n`, and two
(labelled `x` = `false`, `y` = `true`) for each pair `m < n`. -/
abbrev FiducialIndex (N : ℕ) : Type :=
  Fin N ⊕ ({p : Fin N × Fin N // p.1 < p.2} × Bool)

/-- Hardy's `N²` fiducial projectors (Hardy 2001, Eqs. (26)–(27)):
`|n⟩⟨n|` for `n = 1, …, N`, and `|mn⟩ₓ⟨mn|`, `|mn⟩_y⟨mn|` for `m < n`. -/
noncomputable def fiducialProjector {N : ℕ} : FiducialIndex N → Matrix (Fin N) (Fin N) ℂ
  | Sum.inl n => proj (ket n)
  | Sum.inr (p, false) => proj (ketX p.1.1 p.1.2)
  | Sum.inr (p, true) => proj (ketY p.1.1 p.1.2)

end HardyFiveAxioms

Source

L. Hardy, *Quantum Theory From Five Reasonable Axioms*, arXiv:quant-ph/0101012v4 (2001), https://arxiv.org/abs/quant-ph/0101012, p. 8, Section 5, Eqs. (26)–(27) and the surrounding text

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.

Fix $N\in\mathbb N$ and index coordinates by $\{0,\dots,N-1\}$ .

$\mathrm{ket}(n)\in\mathbb C^N$ is the standard unit vector $e_n$ .
$\mathrm{ketX}(m,n)=\frac1{\sqrt2}(e_m+e_n)$ and $\mathrm{ketY}(m,n)=\frac1{\sqrt2}(e_m+i\,e_n)$ , for arbitrary indices $m,n$ . No order or distinctness of $m,n$ is required here. If $m=n$ , then $\mathrm{ketX}(n,n)=\sqrt2\,e_n$ , which is not a unit vector.
For $v\in\mathbb C^N$ , $\mathrm{proj}(v)$ is the $N\times N$ complex matrix with $(j,k)$ entry $v_j\,\overline{v_k}$ . It is the rank-one operator $|v\rangle\langle v|$ , and it is idempotent only when $\|v\|=1$ .
The index type is the disjoint union of $\{0,\dots,N-1\}$ with the product of $\{(m,n): m<n\}$ and $\{\text{false},\text{true}\}$ .
The family $\mathrm{fid}$ sends an index $n$ of the first kind to $\mathrm{proj}(e_n)$ , a pair $(m,n)$ with label false to $\mathrm{proj}(\mathrm{ketX}(m,n))$ , and a pair $(m,n)$ with label true to $\mathrm{proj}(\mathrm{ketY}(m,n))$ . Because $m<n$ , these vectors are unit vectors.

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

Hardy's N2N^2N2 fiducial projectors ∣n⟩⟨n∣|n\rangle\langle n|∣n⟩⟨n∣, ∣mn⟩x⟨mn∣|mn\rangle_x\langle mn|∣mn⟩x​⟨mn∣, ∣mn⟩y⟨mn∣|mn\rangle_y\langle mn|∣mn⟩y​⟨mn∣

Hardy's $N^2$ fiducial projectors $|n\rangle\langle n|$ , $|mn\rangle_x\langle mn|$ , $|mn\rangle_y\langle mn|$