Theorem 3.1: extreme qubit couplings with maximally mixed marginals

Open

QAlgorithms.Papers.Independent.Intakethird100.P12.maximally_mixed_qubit_extreme_iff

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Use the fixed computational basis $|0\rangle,|1\rangle$ in the first copy of $\mathbb C^2$ . Let $\rho$ be a density matrix on $\mathbb C^2\otimes\mathbb C^2$ with both marginals $I_2/2$ , and write $C(I_2/2,I_2/2)$ for all such states. Then

\rho\in\operatorname{Ext}_{\mathbb R}C(I_2/2,I_2/2)\quad\Longleftrightarrow\quad\exists\text{ an orthonormal basis }(\psi_0,\psi_1)\text{ of }\mathbb C^2:\ \rho=|\Omega\rangle\langle\Omega|,

where the vector is constructed from that basis by

|\Omega\rangle=\frac{|0\rangle\otimes|\psi_0\rangle+|1\rangle\otimes|\psi_1\rangle}{\sqrt2}.

Thus the extreme couplings with these marginals are exactly the indicated maximally entangled pure states. The basis is allowed to be complex, and the density-matrix equality is insensitive to global phase.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P12

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- Theorem 3.1, PDF p.9, completed PDF pp.12–13. Density equality absorbs global phase.
The basis witness is genuinely orthonormal over C. Omega is constructed from it.
The proof's rank-two contradiction is not an assumption. -/
theorem maximally_mixed_qubit_extreme_iff
    (rho : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ)
    (hmem : rho ∈ finiteCouplingSet ((1 / 2 : ℂ) • (1 : Matrix (Fin 2) (Fin 2) ℂ))
      ((1 / 2 : ℂ) • (1 : Matrix (Fin 2) (Fin 2) ℂ))) :
    rho ∈ Set.extremePoints ℝ
      (finiteCouplingSet ((1 / 2 : ℂ) • (1 : Matrix (Fin 2) (Fin 2) ℂ))
        ((1 / 2 : ℂ) • (1 : Matrix (Fin 2) (Fin 2) ℂ))) ↔
      ∃ psi : OrthonormalBasis (Fin 2) ℂ (EuclideanSpace ℂ (Fin 2)),
        rho = pureDensity (omegaFromBasis psi) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P12

Source

Extremal Quantum States in Coupled Systems, arXiv:quant-ph/0307182v1, PDF p. 9, Theorem 3.1: extreme qubit couplings with both marginals I/2

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $\rho$ be any complex matrix indexed by $\{0,1\}\times\{0,1\}$ , and suppose $\rho$ belongs to the set $C$ of positive semidefinite matrices $\sigma$ with trace $1$ whose two partial traces both equal $\tfrac12 I_2$ ; explicitly,

\sum_{j=0}^{1}\sigma_{(i,j),(i',j)}=\tfrac12\delta_{i,i'}, \qquad \sum_{i=0}^{1}\sigma_{(i,j),(i,j')}=\tfrac12\delta_{j,j'}.

Then $\rho$ is an extreme point of $C$ over the real numbers if and only if there exists an orthonormal basis $(\psi_0,\psi_1)$ of the complex Euclidean space $\mathbb C^2$ such that

\rho_{(a,b),(c,d)} =\Omega_{(a,b)}\,\overline{\Omega_{(c,d)}} \quad\text{for all }a,b,c,d\in\{0,1\}, \qquad \Omega=\frac{e_0\otimes\psi_0+e_1\otimes\psi_1}{\sqrt2}.

Here $e_0,e_1$ are the standard coordinate vectors, and $(u\otimes v)_{(a,b)}=u_a v_b$ ; thus $\Omega_{(a,b)}=\psi_a(b)/\sqrt2$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph