Prove2Me

N=3N=3: the 9×99\times9 matrix DD with h=12h=\tfrac12, q=14q=\tfrac14

Proved
HardyFiveAxioms.qutrit_D_matrix

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

For N=3N=3, order the fiducial projectors (26)–(27) as

1, 2, 3, 12x, 12y, 13x, 13y, 23x, 23y.1,\ 2,\ 3,\ 12x,\ 12y,\ 13x,\ 13y,\ 23x,\ 23y .

Then the matrix Dij=tr(P^iP^j)D_{ij}=\mathrm{tr}(\hat P_i\hat P_j) is

D=(100hhhh00010hh00hh00100hhhhhh01hqqqqhh0h1qqqqh0hqq1hqqh0hqqh1qq0hhqqqq1h0hhqqqqh1),h=12, q=14.D=\begin{pmatrix} 1&0&0&h&h&h&h&0&0\\ 0&1&0&h&h&0&0&h&h\\ 0&0&1&0&0&h&h&h&h\\ h&h&0&1&h&q&q&q&q\\ h&h&0&h&1&q&q&q&q\\ h&0&h&q&q&1&h&q&q\\ h&0&h&q&q&h&1&q&q\\ 0&h&h&q&q&q&q&1&h\\ 0&h&h&q&q&q&q&h&1 \end{pmatrix},\qquad h=\tfrac12,\ q=\tfrac14 .

In Section 8.7 Hardy derives this matrix from the axioms and states that "the projection operators which give rise to this DD are, up to arbitrary choices in phase, those in equations (26) and (27)". This milestone checks that statement.

Formalization Note Indices are 00-based. The equality is entrywise in C\mathbb C.

Preamble
import Mathlib
import Definitions.Def_hardy2001_projectors
Formal statement
namespace HardyFiveAxioms

/-- Hardy 2001, Section 8.7: for `N = 3` with fiducial order
`1, 2, 3, 12x, 12y, 13x, 13y, 23x, 23y`, the matrix `Dᵢⱼ = tr(P̂ᵢP̂ⱼ)` of the projectors
(26)–(27) has the stated form with `h = 1/2` and `q = 1/4`. -/
theorem qutrit_D_matrix :
    let P : Fin 9 → Matrix (Fin 3) (Fin 3) ℂ :=
      ![proj (ket 0), proj (ket 1), proj (ket 2),
        proj (ketX 0 1), proj (ketY 0 1), proj (ketX 0 2), proj (ketY 0 2),
        proj (ketX 1 2), proj (ketY 1 2)]
    let h : ℝ := 1 / 2
    let q : ℝ := 1 / 4
    let D : Matrix (Fin 9) (Fin 9) ℝ :=
      !![1, 0, 0, h, h, h, h, 0, 0;
         0, 1, 0, h, h, 0, 0, h, h;
         0, 0, 1, 0, 0, h, h, h, h;
         h, h, 0, 1, h, q, q, q, q;
         h, h, 0, h, 1, q, q, q, q;
         h, 0, h, q, q, 1, h, q, q;
         h, 0, h, q, q, h, 1, q, q;
         0, h, h, q, q, q, q, 1, h;
         0, h, h, q, q, q, q, h, 1]
    ∀ i j : Fin 9, (P i * P j).trace = (D i j : ℂ) := 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. 22–23, Section 8.7 (the 9×99\times9 matrix DD with h=1/2h=1/2, q=1/4q=1/4)
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 e0,e1,e2e_0,e_1,e_2 be the standard basis of C3\mathbb C^3 and let proj(v)\mathrm{proj}(v) be the 3×33\times3 matrix with entries vjvk‾v_j\overline{v_k}. Define nine matrices P0,…,P8P_0,\dots,P_8 as proj\mathrm{proj} of, in order: e0e_0, e1e_1, e2e_2, 12(e0+e1)\tfrac1{\sqrt2}(e_0+e_1), 12(e0+ie1)\tfrac1{\sqrt2}(e_0+ie_1), 12(e0+e2)\tfrac1{\sqrt2}(e_0+e_2), 12(e0+ie2)\tfrac1{\sqrt2}(e_0+ie_2), 12(e1+e2)\tfrac1{\sqrt2}(e_1+e_2), 12(e1+ie2)\tfrac1{\sqrt2}(e_1+ie_2). With h=12h=\tfrac12 and q=14q=\tfrac14, let DD be the real 9×99\times9 matrix with rows

  • (1,0,0,h,h,h,h,0,0)(1,0,0,h,h,h,h,0,0)
  • (0,1,0,h,h,0,0,h,h)(0,1,0,h,h,0,0,h,h)
  • (0,0,1,0,0,h,h,h,h)(0,0,1,0,0,h,h,h,h)
  • (h,h,0,1,h,q,q,q,q)(h,h,0,1,h,q,q,q,q)
  • (h,h,0,h,1,q,q,q,q)(h,h,0,h,1,q,q,q,q)
  • (h,0,h,q,q,1,h,q,q)(h,0,h,q,q,1,h,q,q)
  • (h,0,h,q,q,h,1,q,q)(h,0,h,q,q,h,1,q,q)
  • (0,h,h,q,q,q,q,1,h)(0,h,h,q,q,q,q,1,h)
  • (0,h,h,q,q,q,q,h,1)(0,h,h,q,q,q,q,h,1).

Then tr(PiPj)=Dij\mathrm{tr}(P_iP_j)=D_{ij}, viewed in C\mathbb C, for all i,j∈{0,…,8}i,j\in\{0,\dots,8\}.

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