The $N=2$ matrices $D$ , $C$ , $A$ and the roots $c_\pm$

Definition

hardy2001_qubit

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

For real parameters $a,b,c$ , Section 8.6 (and Section 5) of the paper consider the $4\times4$ matrix

D=\begin{pmatrix}1&0&1-a&1-b\\0&1&a&b\\1-a&a&1&c\\1-b&b&c&1\end{pmatrix},

the change-of-variables matrix

C=\begin{pmatrix}1&0&0&0\\1&1&0&0\\0&0&1&0\\0&0&0&1\end{pmatrix},

the $3\times3$ matrix

A=\begin{pmatrix}\tfrac12&a-\tfrac12&b-\tfrac12\\a-\tfrac12&\tfrac12&c-\tfrac12\\b-\tfrac12&c-\tfrac12&\tfrac12\end{pmatrix},

and the two numbers

c_\pm=1-a-b+2ab\pm2\sqrt{ab(1-a)(1-b)} .

$D_{ij}$ is the probability of obtaining the $i$ -th fiducial measurement on the $j$ -th fiducial state of a system with $N=2$ , $K=4$ . Pure states then lie on the surface $\vec v^{\,T}A\vec v=\tfrac12$ .

Formalization Note Rows and columns are indexed from $0$ . $\sqrt{\cdot}$ is Real.sqrt, which returns $0$ on negative arguments. Statements that use $c_\pm$ assume $0\le a,b\le1$ , where the radicand is nonnegative.

Definition code

import Mathlib

namespace HardyFiveAxioms

/-- The matrix `D` of the `N = 2`, `K = 4` case (Hardy 2001, Eqs. (34) and (74)), with
fiducial vectors indexed `0, 1, 2, 3` (the paper's `1, 2, 3, 4`). -/
def qubitD (a b c : ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, 0, 1 - a, 1 - b;
     0, 1, a, b;
     1 - a, a, 1, c;
     1 - b, b, c, 1]

/-- The change of variables `r = C v` (Hardy 2001, Eq. (78)). -/
def qubitC : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, 0, 0, 0;
     1, 1, 0, 0;
     0, 0, 1, 0;
     0, 0, 0, 1]

/-- The `3 × 3` matrix `A` of Hardy 2001, Eq. (83). -/
noncomputable def qubitA (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℝ :=
  !![1 / 2, a - 1 / 2, b - 1 / 2;
     a - 1 / 2, 1 / 2, c - 1 / 2;
     b - 1 / 2, c - 1 / 2, 1 / 2]

/-- `c₊ = 1 - a - b + 2ab + 2√(ab(1-a)(1-b))` (Hardy 2001, Eqs. (37) and (85)). -/
noncomputable def cPlus (a b : ℝ) : ℝ :=
  1 - a - b + 2 * a * b + 2 * Real.sqrt (a * b * (1 - a) * (1 - b))

/-- `c₋ = 1 - a - b + 2ab - 2√(ab(1-a)(1-b))` (Hardy 2001, Eqs. (37) and (85)). -/
noncomputable def cMinus (a b : ℝ) : ℝ :=
  1 - a - b + 2 * a * b - 2 * Real.sqrt (a * b * (1 - a) * (1 - b))

end HardyFiveAxioms

Source

L. Hardy, *Quantum Theory From Five Reasonable Axioms*, arXiv:quant-ph/0101012v4 (2001), https://arxiv.org/abs/quant-ph/0101012, p. 9, Eqs. (34), (37); pp. 20–21, Section 8.6, Eqs. (74), (78), (83), (85)

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 real numbers $a,b,c$ (no constraints):

$D(a,b,c)$ is the real $4\times4$ matrix with rows $(1,0,1-a,1-b)$ , $(0,1,a,b)$ , $(1-a,a,1,c)$ , $(1-b,b,c,1)$ . It is symmetric.
$C$ is the real $4\times4$ matrix with rows $(1,0,0,0)$ , $(1,1,0,0)$ , $(0,0,1,0)$ , $(0,0,0,1)$ .
$A(a,b,c)$ is the real symmetric $3\times3$ matrix with diagonal entries $\tfrac12$ , $(1,2)$ entry $a-\tfrac12$ , $(1,3)$ entry $b-\tfrac12$ , and $(2,3)$ entry $c-\tfrac12$ .
$c_+(a,b)=1-a-b+2ab+2\sqrt{ab(1-a)(1-b)}$ and $c_-(a,b)=1-a-b+2ab-2\sqrt{ab(1-a)(1-b)}$ . Here $\sqrt{t}$ is the nonnegative square root for $t\ge0$ and is $0$ for $t<0$ , so outside $0\le a,b\le1$ the radicand may be negative and then $c_+=c_-=1-a-b+2ab$ .

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

The N=2N=2N=2 matrices DDD, CCC, AAA and the roots c±c_\pmc±​

The $N=2$ matrices $D$ , $C$ , $A$ and the roots $c_\pm$