Prove2Me

Qubit overlap: c=1−a−b+2ab+2cos⁡(ϕ4−ϕ3)ab(1−a)(1−b)c=1-a-b+2ab+2\cos(\phi_4-\phi_3)\sqrt{ab(1-a)(1-b)}

Proved
HardyFiveAxioms.qubit_overlap_formula

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

linear-algebramathematical-physicsquantum-foundationsquantum-information

Let 0≤a,b≤10\le a,b\le1 and ϕ3,ϕ4∈R\phi_3,\phi_4\in\mathbb R. Put

α=1−a,β=a eiϕ3,γ=1−b,δ=b eiϕ4,\alpha=\sqrt{1-a},\quad\beta=\sqrt a\,e^{i\phi_3},\quad\gamma=\sqrt{1-b},\quad\delta=\sqrt b\,e^{i\phi_4},

and let P^3=(α∣1⟩+β∣2⟩)(α∗⟨1∣+β∗⟨2∣)\hat P_3=(\alpha|1\rangle+\beta|2\rangle)(\alpha^*\langle1|+\beta^*\langle2|) and P^4=(γ∣1⟩+δ∣2⟩)(γ∗⟨1∣+δ∗⟨2∣)\hat P_4=(\gamma|1\rangle+\delta|2\rangle)(\gamma^*\langle1|+\delta^*\langle2|), as in Eqs. (31)–(32). Then the entry c=D34=tr(P^3P^4)=∣αγ∗+βδ∗∣2c=D_{34}=\mathrm{tr}(\hat P_3\hat P_4)=|\alpha\gamma^*+\beta\delta^*|^2 equals

c=1−a−b+2ab+2cos⁡(ϕ4−ϕ3)ab(1−a)(1−b).c=1-a-b+2ab+2\cos(\phi_4-\phi_3)\sqrt{ab(1-a)(1-b)} .

This is Eq. (35). Varying the phases yields c−≤c≤c+c_-\le c\le c_+.

Formalization Note The paper says α\alpha and γ\gamma "can be chosen real". The statement takes the nonnegative real choice α=1−a\alpha=\sqrt{1-a}, γ=1−b\gamma=\sqrt{1-b}. The paper's δ=bexp⁡(ϕ4)\delta=\sqrt b\exp(\phi_4) is read as b eiϕ4\sqrt b\,e^{i\phi_4}, an evident typo. The trace is computed in Lean for proj(v)=∣v⟩⟨v∣\mathrm{proj}(v)=|v\rangle\langle v|.

Preamble
import Mathlib
import Definitions.Def_hardy2001_projectors
Formal statement
namespace HardyFiveAxioms

/-- Hardy 2001, Section 5, Eqs. (31)–(35): with `α = √(1-a)`, `β = √a e^{iφ₃}`,
`γ = √(1-b)`, `δ = √b e^{iφ₄}`, the entry `c = tr(P̂₃P̂₄) = |αγ* + βδ*|²` of `D` equals
`1 - a - b + 2ab + 2 cos(φ₄ - φ₃) √(ab(1-a)(1-b))`. -/
theorem qubit_overlap_formula (a b φ₃ φ₄ : ℝ) (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1)
    (hb₀ : 0 ≤ b) (hb₁ : b ≤ 1) :
    (proj ![(Real.sqrt (1 - a) : ℂ), (Real.sqrt a : ℂ) * Complex.exp (φ₃ * Complex.I)] *
        proj ![(Real.sqrt (1 - b) : ℂ), (Real.sqrt b : ℂ) * Complex.exp (φ₄ * Complex.I)]).trace =
      ((1 - a - b + 2 * a * b + 2 * Real.cos (φ₄ - φ₃) * Real.sqrt (a * b * (1 - a) * (1 - 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. (31)–(35)
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,ϕ3,ϕ4a,b,\phi_3,\phi_4 be real numbers with 0≤a≤10\le a\le1 and 0≤b≤10\le b\le1. Let u=(1−a, a eiϕ3)∈C2u=(\sqrt{1-a},\ \sqrt a\,e^{i\phi_3})\in\mathbb C^2 and w=(1−b, b eiϕ4)∈C2w=(\sqrt{1-b},\ \sqrt b\,e^{i\phi_4})\in\mathbb C^2, with nonnegative real square roots. Let proj(u)\mathrm{proj}(u) be the 2×22\times2 matrix with entries ujuk‾u_j\overline{u_k}, and similarly proj(w)\mathrm{proj}(w). Then the trace of the matrix product satisfies

tr(proj(u) proj(w))=1−a−b+2ab+2cos⁡(ϕ4−ϕ3)ab(1−a)(1−b),\mathrm{tr}\big(\mathrm{proj}(u)\,\mathrm{proj}(w)\big)=1-a-b+2ab+2\cos(\phi_4-\phi_3)\sqrt{ab(1-a)(1-b)} ,

as an equality of complex numbers, with the right-hand side a real number viewed as complex.

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