Theorem 2.5: general extremality criterion and rank bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P12.general_extremality_criterion

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

prove2quantum

Let $d_1,d_2$ be the dimensions of finite-dimensional complex Hilbert spaces with chosen orthonormal bases. Let $\rho_1,\rho_2$ be positive semidefinite operators of trace one. Write $C(\rho_1,\rho_2)$ for all joint density matrices with these two partial traces, and $E(\rho_1,\rho_2)$ for its extreme points over the real scalars. Coordinates in the tensor product use lexicographic order.

For every $\rho\in C(\rho_1,\rho_2)$ of rank $k$ , extremality necessarily implies

k\le\sqrt{d_1^2+d_2^2-1}.

For every rank-block representation below, allowing $k=n$ and then a zero-column $A$ , the following criterion holds.

Set $n=d_1d_2$ and $k=\operatorname{rank}\rho$ . Let $\sigma$ be a permutation unitary, $A$ a complex $k\times(n-k)$ matrix, and $K$ a strictly positive definite $k\times k$ matrix satisfying

\sigma\rho\sigma^{-1}=B_A(K),\qquad B_A(L)=\begin{pmatrix}L&LA\\A^\dagger L&A^\dagger LA\end{pmatrix}.

Here $\dagger$ denotes conjugate transpose. Both marginals of $\sigma^{-1}B_A(L)\sigma$ are computed in the original tensor coordinates.

Put $R=[I_k\mid A]$ and

D=\{R\sigma(X_1\otimes I_{d_2}+I_{d_1}\otimes X_2)\sigma^{-1}R^\dagger:X_1=X_1^\dagger,\ X_2=X_2^\dagger\}.

Then

\rho\in E(\rho_1,\rho_2)\quad\Longleftrightarrow\quad D=\operatorname{Herm}(k),

where $\operatorname{Herm}(k)$ is the real vector space of all Hermitian matrices of order $k$ . This characterizes extremality by a concrete finite-dimensional image and also bounds the possible ranks.

Formalization Note The printed column $[I;A^t]$ is changed to $[I;A^\dagger]$ , following (2.11) on PDF p.6 and the $AXA^\dagger$ expansion on PDF p.11. This correction requires independent moderation.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P12

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- Theorem 2.5, PDF pp.7–8: BOTH the rank bound and full iff criterion.
Printed D ends with [I;A^t]; changed to [I;A†], required by (2.11), PDF p.6,
and the AXA† expansion, PDF p.11. Independent moderation of this correction is pending.
Here k=n is allowed, with zero-column A. -/
theorem general_extremality_criterion {d1 d2 k : ℕ}
    (rho1 : Matrix (Fin d1) (Fin d1) ℂ) (rho2 : Matrix (Fin d2) (Fin d2) ℂ)
    (hm1 : IsDensityMatrix rho1) (hm2 : IsDensityMatrix rho2)
    (rho : Matrix (Fin d1 × Fin d2) (Fin d1 × Fin d2) ℂ)
    (hmem : rho ∈ finiteCouplingSet rho1 rho2) (hrank : rho.rank = k) :
    (rho ∈ Set.extremePoints ℝ (finiteCouplingSet rho1 rho2) →
      (k : ℝ) ≤ Real.sqrt ((d1 : ℝ)^2 + (d2 : ℝ)^2 - 1)) ∧
    ∀ (hkn : k ≤ d1*d2) (p : Equiv.Perm (Fin (d1*d2)))
      (A : Matrix (Fin k) (Fin (d1*d2-k)) ℂ) (K : Matrix (Fin k) (Fin k) ℂ),
      K.PosDef → permuteMatrix p (flatMatrix rho) = rankBlockMatrix hkn K A →
      (rho ∈ Set.extremePoints ℝ (finiteCouplingSet rho1 rho2) ↔
        compressedLocalSpace hkn p A = {L | L.IsHermitian}) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P12

Source

Extremal Quantum States in Coupled Systems, arXiv:quant-ph/0307182v1, PDF p. 7, Theorem 2.5: general extremality criterion and rank bound (original abstract seed)

Read-back

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

For any natural numbers $d_1,d_2,k$ , let $\rho_1,\rho_2$ be complex positive semidefinite matrices of sizes $d_1,d_2$ , each with trace $1$ . Let $C$ be the set of positive semidefinite, trace- $1$ matrices $\sigma$ on the product index set satisfying $\sum_j\sigma_{(i,j),(i',j)}=(\rho_1)_{i,i'}$ and $\sum_i\sigma_{(i,j),(i,j')}=(\rho_2)_{j,j'}$ for all appropriate indices. Suppose $\rho\in C$ and $\operatorname{rank}_{\mathbb C}(\rho)=k$ . Then the following conjunction holds: if $\rho$ is an extreme point of $C$ over the real numbers, then

k\le\sqrt{d_1^2+d_2^2-1};

and, for every inequality $k\le n:=d_1d_2$ , every permutation $p$ of $\{0,\ldots,n-1\}$ , every complex $k\times(n-k)$ matrix $A$ , and every complex $k\times k$ matrix $K$ , if $K$ is positive definite and

F_p(\rho)= \begin{pmatrix}K&KA\\A^*K&A^*KA\end{pmatrix},

then $\rho$ is an extreme point of $C$ if and only if

\left\{ R\,F_p(X_1\otimes I_{d_2}+I_{d_1}\otimes X_2)\,R^* \ \middle|\ X_1=X_1^*\in\mathbb C^{d_1\times d_1},\ X_2=X_2^*\in\mathbb C^{d_2\times d_2} \right\} = \{L\in\mathbb C^{k\times k}:L=L^*\}.

Here $\beta(i,j)=id_2+j$ , $F_p(M)_{u,v}=M_{\beta^{-1}(p(u)),\beta^{-1}(p(v))}$ , $R=[\,I_k\ \ A\,]$ , and $^{*}$ denotes conjugate transpose; the displayed block matrix uses the first $k$ and last $n-k$ coordinates. The universal statement includes $k=n$ , in which case $A$ has no columns and $R=I_n$ . The trace- $1$ and rank hypotheses rule out $k=0$ and zero marginal dimensions.

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