Arbitrary qubit marginals: extreme couplings have rank one or two

Open

QAlgorithms.Papers.Independent.Intakethird100.P12.two_qubit_extremal_rank

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

prove2quantum

Let $\rho_1,\rho_2$ be arbitrary density matrices on $\mathbb C^2$ . Let $C(\rho_1,\rho_2)$ contain all joint density matrices on $\mathbb C^2\otimes\mathbb C^2$ with those partial traces. Every real convex extreme point $\rho$ of this set satisfies

\operatorname{rank}\rho\in\{1,2\}.

This specializes the general bound $\sqrt7$ to two qubits; trace one excludes rank zero. The marginals need not be maximally mixed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P12

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- Section 3, PDF pp.8–9: arbitrary qubit marginals, before specializing to I/2. -/
theorem two_qubit_extremal_rank (rho1 rho2 : Matrix (Fin 2) (Fin 2) ℂ)
    (hm1 : IsDensityMatrix rho1) (hm2 : IsDensityMatrix rho2)
    (rho : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ)
    (hext : rho ∈ Set.extremePoints ℝ (finiteCouplingSet rho1 rho2)) :
    rho.rank = 1 ∨ rho.rank = 2 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P12

Source

Extremal Quantum States in Coupled Systems, arXiv:quant-ph/0307182v1, PDF p. 9, Unnumbered rank-1-or-2 consequence for arbitrary qubit marginals

Read-back

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

Let $\rho_1,\rho_2$ be any complex $2\times2$ positive semidefinite matrices with trace $1$ . Let $C$ consist of all complex positive semidefinite matrices $\sigma$ , indexed by $\{0,1\}\times\{0,1\}$ , with trace $1$ and satisfying

\sum_{j=0}^{1}\sigma_{(i,j),(i',j)}=(\rho_1)_{i,i'}, \qquad \sum_{i=0}^{1}\sigma_{(i,j),(i,j')}=(\rho_2)_{j,j'}

for all $i,i',j,j'\in\{0,1\}$ . For every matrix $\rho$ that is an extreme point of $C$ over the real numbers, its complex matrix rank is exactly $1$ or exactly $2$ :

\operatorname{rank}_{\mathbb C}(\rho)=1 \quad\lor\quad \operatorname{rank}_{\mathbb C}(\rho)=2.

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