Hardy's $N^2$ fiducial projectors are linearly independent

Proved

HardyFiveAxioms.fiducialProjector_card_linearIndependent

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

For every $N$ , there are exactly $N^2$ fiducial projectors

|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),

and they are linearly independent over $\mathbb R$ as elements of the space of complex $N\times N$ matrices.

This is the claim of Section 5 that "this makes a total of $N^2$ projectors. It is clear that these projectors are linearly independent."

Formalization Note Linear independence is over $\mathbb R$ , the field relevant to real combinations $a\cdot\hat P$ of Hermitian operators. The count refers to the index type of the family in hardy2001_projectors.

Preamble

import Mathlib
import Definitions.Def_hardy2001_projectors

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 5 (Eqs. (26)–(27)): there are `N²` fiducial projectors
`|n⟩⟨n|`, `|mn⟩ₓ⟨mn|`, `|mn⟩_y⟨mn|`, and they are linearly independent over `ℝ`. -/
theorem fiducialProjector_card_linearIndependent (N : ℕ) :
    Fintype.card (FiducialIndex N) = N ^ 2 ∧
      LinearIndependent ℝ (fiducialProjector (N := N)) := 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. 8, Section 5, Eqs. (26)–(27) and the sentences following Eq. (27)

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.

For every natural number $N$ , two things hold. First, the index set of the fiducial family (the disjoint union of $\{0,\dots,N-1\}$ with two copies of the set of pairs $(m,n)$ , $0\le m<n\le N-1$ ) has exactly $N^2$ elements. Second, the family $\mathrm{fid}$ of complex $N\times N$ matrices, consisting of $\mathrm{proj}(e_n)$ , $\mathrm{proj}(\tfrac1{\sqrt2}(e_m+e_n))$ and $\mathrm{proj}(\tfrac1{\sqrt2}(e_m+ie_n))$ for $m<n$ , is linearly independent over $\mathbb R$ : a real linear combination of these matrices is the zero matrix only if all coefficients are $0$ . Here $\mathrm{proj}(v)_{jk}=v_j\overline{v_k}$ .

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 are linearly independent

Hardy's $N^2$ fiducial projectors are linearly independent