Qubit: $r^TDr'=\vec v^{\,T}A\vec v\,'+\mu\mu'/2$

Proved

HardyFiveAxioms.qubit_bilinear_decomposition

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

linear-algebramathematical-physicsquantum-foundations

Let $a,b,c\in\mathbb R$ , let $v=(v_0,v_1,v_2,v_3)$ and $v'=(v_0',v_1',v_2',v_3')$ be real vectors, and put $r=Cv$ and $r'=Cv'$ , with $C$ as in Eq. (78). Then

r^TD\,r'=\vec v^{\,T}A\,\vec v\,'+\frac{\mu\mu'}2,

where $\vec v=(v_1,v_2,v_3)$ , $\vec v\,'=(v_1',v_2',v_3')$ , $D$ is the matrix (74), $A$ is the matrix (83), and

\mu=2v_0+v_1+v_2+v_3,\qquad \mu'=2v_0'+v_1'+v_2'+v_3'

are the normalization coefficients of Eq. (80).

This is Eq. (81) of the paper, the identity that turns the pure-state condition $r^TDr=1$ for normalized states into the quadric $\vec v^{\,T}A\vec v=\tfrac12$ (Eq. (84)).

Preamble

import Mathlib
import Definitions.Def_hardy2001_qubit

Formal statement

namespace HardyFiveAxioms

open Matrix

/-- Hardy 2001, Section 8.6, Eqs. (76)–(83): writing `r = C v`, `r' = C v'`, the bilinear
form satisfies `rᵀ D r' = v⃗ᵀ A v⃗' + μ μ'/2`, where `v⃗ = (v₁, v₂, v₃)` and
`μ = 2v₀ + v₁ + v₂ + v₃` is the normalization coefficient (Eq. (80)). -/
theorem qubit_bilinear_decomposition (a b c : ℝ) (v w : Fin 4 → ℝ) :
    (qubitC *ᵥ v) ⬝ᵥ (qubitD a b c *ᵥ (qubitC *ᵥ w)) =
      ![v 1, v 2, v 3] ⬝ᵥ (qubitA a b c *ᵥ ![w 1, w 2, w 3]) +
        (2 * v 0 + v 1 + v 2 + v 3) * (2 * w 0 + w 1 + w 2 + w 3) / 2 := 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. 21, Section 8.6, Eqs. (76)–(83)

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 all real numbers $a,b,c$ and all vectors $v,w\in\mathbb R^4$ (coordinates $v_0,\dots,v_3$ and $w_0,\dots,w_3$ ):

(Cv)\cdot\big(D\,(Cw)\big)=(v_1,v_2,v_3)\cdot\big(A\,(w_1,w_2,w_3)\big)+\frac{(2v_0+v_1+v_2+v_3)(2w_0+w_1+w_2+w_3)}{2},

where $\cdot$ is the standard dot product. Here $C$ has rows $(1,0,0,0)$ , $(1,1,0,0)$ , $(0,0,1,0)$ , $(0,0,0,1)$ , $D=D(a,b,c)$ has rows $(1,0,1-a,1-b)$ , $(0,1,a,b)$ , $(1-a,a,1,c)$ , $(1-b,b,c,1)$ , and $A=A(a,b,c)$ is the symmetric $3\times3$ matrix with diagonal $\tfrac12$ and off-diagonal entries $a-\tfrac12$ (positions 1,2), $b-\tfrac12$ (positions 1,3) and $c-\tfrac12$ (positions 2,3). No constraints on $a,b,c$ are imposed.

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

Qubit: rTDr′=v⃗ TAv⃗ ′+μμ′/2r^TDr'=\vec v^{\,T}A\vec v\,'+\mu\mu'/2rTDr′=vTAv′+μμ′/2

Qubit: $r^TDr'=\vec v^{\,T}A\vec v\,'+\mu\mu'/2$