Qubit: $\det D>0\iff c_-<c<c_+$

Proved

HardyFiveAxioms.qubitD_det_pos_iff

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

Let $0\le a,b\le1$ and $c\in\mathbb R$ , and let $D=D(a,b,c)$ be the $4\times4$ matrix of Eq. (34)/(74). Then

\det D>0\iff c_-<c<c_+,\qquad c_\pm=1-a-b+2ab\pm2\sqrt{ab(1-a)(1-b)} .

In Section 5 Hardy observes that the quantum constraint $c_-<c<c_+$ (Eqs. (36)–(37)) "is equivalent to the condition $\mathrm{Det}(D)>0$ ". In Section 8.6 he notes that $\det D=0$ has the same roots $c_\pm$ as $\det A=0$ .

Formalization Note At the boundary $a\in\{0,1\}$ or $b\in\{0,1\}$ one has $c_-=c_+$ , so the interval is empty and $\det D\le0$ .

Preamble

import Mathlib
import Definitions.Def_hardy2001_qubit

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 5, Eqs. (36)–(37) (and Section 8.6, Eq. (85)): for `0 ≤ a, b ≤ 1`,
`det D > 0` if and only if `c₋ < c < c₊`. -/
theorem qubitD_det_pos_iff (a b c : ℝ) (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) (hb₀ : 0 ≤ b) (hb₁ : b ≤ 1) :
    0 < (qubitD a b c).det ↔ cMinus a b < c ∧ c < cPlus a b := 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. 9, Section 5, Eqs. (34), (36)–(37) and the sentence after (37); p. 21, Section 8.6, after Eq. (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.

Let $a,b,c$ be real numbers with $0\le a\le1$ and $0\le b\le1$ . Let $D$ be 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)$ . Then $\det D>0$ holds if and only if both $1-a-b+2ab-2\sqrt{ab(1-a)(1-b)}<c$ and $c<1-a-b+2ab+2\sqrt{ab(1-a)(1-b)}$ hold. Under the stated bounds the radicand is nonnegative.

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: det⁡D>0 ⟺ c−<c<c+\det D>0\iff c_-<c<c_+detD>0⟺c−​<c<c+​

Qubit: $\det D>0\iff c_-<c<c_+$