Proposition 2.3: necessity of the zero-marginal perturbation criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P12.zero_marginal_necessity

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.

Let $\rho\in C(\rho_1,\rho_2)$ have rank $k<n$ .

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.

If $\rho$ is extreme, then for every Hermitian matrix $L$ of order $k$ ,

\operatorname{Tr}_{H_2}(\sigma^{-1}B_A(L)\sigma)=0\ \text{and}\ \operatorname{Tr}_{H_1}(\sigma^{-1}B_A(L)\sigma)=0\quad\Longrightarrow\quad L=0.

Thus an extreme coupling admits no nonzero Hermitian perturbation in its rank-block coordinates that preserves both marginals.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P12

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- Proposition 2.3, PDF pp.5–6: extremality implies injectivity on Hermitian perturbations. -/
theorem zero_marginal_necessity {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)
    (hkn : k < d1*d2) (p : Equiv.Perm (Fin (d1*d2)))
    (A : Matrix (Fin k) (Fin (d1*d2-k)) ℂ) (K : Matrix (Fin k) (Fin k) ℂ)
    (hK : K.PosDef) (hblock : permuteMatrix p (flatMatrix rho) = rankBlockMatrix hkn.le K A)
    (hext : rho ∈ Set.extremePoints ℝ (finiteCouplingSet rho1 rho2)) :
    NoZeroMarginalPerturbation hkn.le p A := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P12

Source

Extremal Quantum States in Coupled Systems, arXiv:quant-ph/0307182v1, PDF p. 5, Proposition 2.3: necessity of the zero-marginal perturbation criterion

Read-back

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

For all natural numbers $d_1,d_2,k$ , let $\rho_1,\rho_2$ be complex matrices of sizes $d_1\times d_1$ and $d_2\times d_2$ , each positive semidefinite with trace one. Let $\rho$ be a complex matrix on the product index set, also positive semidefinite with trace one, whose partial traces satisfy $\sum_b\rho_{(a,b),(a',b)}=(\rho_1)_{a,a'}$ and $\sum_a\rho_{(a,b),(a,b')}=(\rho_2)_{b,b'}$ . Assume that $\operatorname{rank}\rho=k<d_1d_2$ . Let $p$ be any permutation of $\{0,\ldots,d_1d_2-1\}$ , let $A$ be a complex $k\times(d_1d_2-k)$ matrix, and let $K$ be a positive definite complex $k\times k$ matrix. Writing $f(a,b)=d_2a+b$ and

B_A(H)= \begin{pmatrix} H & HA\\ A^\dagger H & A^\dagger HA \end{pmatrix},

assume that $\rho_{f^{-1}(p(i)),\,f^{-1}(p(j))}=B_A(K)_{i,j}$ for all $i,j$ . Also assume that $\rho$ is an extreme point, with respect to real scalars, of the set of positive semidefinite trace-one matrices with these same two partial traces: whenever $\rho=t\sigma+(1-t)\tau$ for $0<t<1$ and $\sigma,\tau$ in that set, one has $\sigma=\tau=\rho$ . Then every Hermitian complex $k\times k$ matrix $L$ for which the matrix

(P_L)_{(a,b),(a',b')}=B_A(L)_{p^{-1}(f(a,b)),\,p^{-1}(f(a',b'))}

has both partial traces zero must itself satisfy $L=0$ . The assumptions cannot hold when either $d_1$ or $d_2$ is zero, or when $k=0$ , because $\rho$ has trace one.

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