Bloch sphere: $D_{ij}=\mathrm{tr}(\hat P_i\hat P_j)$ for $N=2$ with $a=b=c=\tfrac12$

Proved

HardyFiveAxioms.bloch_D_matrix

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

For $N=2$ , take the fiducial projectors $\hat P_1=|1\rangle\langle1|$ , $\hat P_2=|2\rangle\langle2|$ , $\hat P_3=|12\rangle_x\langle12|$ , $\hat P_4=|12\rangle_y\langle12|$ of Eqs. (26)–(27). Then the matrix $D_{ij}=\mathrm{tr}(\hat P_i\hat P_j)$ of Eq. (18) is

D=\begin{pmatrix}1&0&\tfrac12&\tfrac12\\0&1&\tfrac12&\tfrac12\\\tfrac12&\tfrac12&1&\tfrac12\\\tfrac12&\tfrac12&\tfrac12&1\end{pmatrix},

which is Eq. (87), the choice $a=b=c=\tfrac12$ for which the pure-state surface is the Bloch sphere.

Formalization Note Indices are $0$ -based. The equality is entrywise in $\mathbb C$ , with the real entries cast to complex numbers.

Preamble

import Mathlib
import Definitions.Def_hardy2001_projectors

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Eq. (87) (with Eqs. (18), (26)–(27)): for `N = 2` and the fiducial projectors
`|1⟩⟨1|`, `|2⟩⟨2|`, `|12⟩ₓ⟨12|`, `|12⟩_y⟨12|`, the matrix `Dᵢⱼ = tr(P̂ᵢP̂ⱼ)` is the
Bloch-sphere matrix with `a = b = c = 1/2`. -/
theorem bloch_D_matrix :
    let P : Fin 4 → Matrix (Fin 2) (Fin 2) ℂ :=
      ![proj (ket 0), proj (ket 1), proj (ketX 0 1), proj (ketY 0 1)]
    ∀ i j : Fin 4, (P i * P j).trace =
      ((!![1, 0, 1 / 2, 1 / 2;
           0, 1, 1 / 2, 1 / 2;
           1 / 2, 1 / 2, 1, 1 / 2;
           1 / 2, 1 / 2, 1 / 2, 1] : Matrix (Fin 4) (Fin 4) ℝ) 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, p. 7, Eq. (18); p. 8, Eqs. (26)–(27); p. 22, Section 8.6, Eq. (87)

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 $P_0,P_1,P_2,P_3$ be the complex $2\times2$ matrices $\mathrm{proj}(e_0)$ , $\mathrm{proj}(e_1)$ , $\mathrm{proj}(\tfrac1{\sqrt2}(e_0+e_1))$ and $\mathrm{proj}(\tfrac1{\sqrt2}(e_0+ie_1))$ , where $\mathrm{proj}(v)_{jk}=v_j\overline{v_k}$ and $e_0,e_1$ is the standard basis of $\mathbb C^2$ . Then for all $i,j\in\{0,1,2,3\}$ , $\mathrm{tr}(P_iP_j)=M_{ij}$ , where $M$ is the real matrix with rows $(1,0,\tfrac12,\tfrac12)$ , $(0,1,\tfrac12,\tfrac12)$ , $(\tfrac12,\tfrac12,1,\tfrac12)$ , $(\tfrac12,\tfrac12,\tfrac12,1)$ , viewed in $\mathbb C$ .

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

Bloch sphere: Dij=tr(P^iP^j)D_{ij}=\mathrm{tr}(\hat P_i\hat P_j)Dij​=tr(P^i​P^j​) for N=2N=2N=2 with a=b=c=12a=b=c=\tfrac12a=b=c=21​

Bloch sphere: $D_{ij}=\mathrm{tr}(\hat P_i\hat P_j)$ for $N=2$ with $a=b=c=\tfrac12$