Every Hermitian operator is a real combination of the fiducial projectors

Proved

HardyFiveAxioms.hermitian_mem_span_fiducialProjector

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

Every Hermitian $N\times N$ complex matrix $\hat A$ can be written as a real linear combination

\hat A=\sum_k a_k\hat P_k,\qquad a_k\in\mathbb R,

of Hardy's fiducial projectors $|n\rangle\langle n|$ , $|mn\rangle_x\langle mn|$ , $|mn\rangle_y\langle mn|$ .

Section 5 uses this to represent states and measurements by real vectors: "Any Hermitean matrix can be written as a sum of these projection operators times real numbers, i.e. in the form $a\cdot\hat P$ ." Together with linear independence it shows that the $N^2$ projectors form a real basis of the Hermitian operators.

Preamble

import Mathlib
import Definitions.Def_hardy2001_projectors

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 5: every Hermitian operator on `ℂᴺ` is a real linear combination of
the fiducial projectors `|n⟩⟨n|`, `|mn⟩ₓ⟨mn|`, `|mn⟩_y⟨mn|`. -/
theorem hermitian_mem_span_fiducialProjector (N : ℕ) (A : Matrix (Fin N) (Fin N) ℂ)
    (hA : A.IsHermitian) :
    A ∈ Submodule.span ℝ (Set.range (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, pp. 6–8, Section 5 (paragraph before Eq. (11), text after Eq. (11), and Eqs. (26)–(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$ and every complex $N\times N$ matrix $A$ that is Hermitian ( $A$ equals its conjugate transpose), $A$ belongs to the real linear span of the matrices $\mathrm{fid}(i)$ . That is, $A=\sum_i a_i\,\mathrm{fid}(i)$ for some real coefficients $a_i$ , where $\mathrm{fid}$ consists of $\mathrm{proj}(e_n)$ , $\mathrm{proj}(\tfrac1{\sqrt2}(e_m+e_n))$ and $\mathrm{proj}(\tfrac1{\sqrt2}(e_m+ie_n))$ ( $m<n$ ) as in hardy2001_projectors.

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