Proposition 2.4: sufficiency of the zero-marginal perturbation criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P12.zero_marginal_sufficiency

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.

Suppose that every Hermitian matrix $L$ of order $k$ satisfies

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

Then

\rho\in E(\rho_1,\rho_2).

This supplies the converse to the necessary perturbation condition, without assuming any factorization of midpoint summands.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P12

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- Proposition 2.4, PDF p.7: injectivity is a hypothesis, extremality the conclusion.
No midpoint factorization is imposed as an additional hypothesis. -/
theorem zero_marginal_sufficiency {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)
    (hinjective : NoZeroMarginalPerturbation hkn.le p A) :
    rho ∈ Set.extremePoints ℝ (finiteCouplingSet rho1 rho2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P12

Source

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

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$ , and let $C$ consist of all positive semidefinite matrices $\sigma$ of trace $1$ on the product index set whose two partial traces are $\rho_1,\rho_2$ ; explicitly, these partial traces have entries $\sum_j\sigma_{(i,j),(i',j)}$ and $\sum_i\sigma_{(i,j),(i,j')}$ , respectively. Suppose $\rho\in C$ , $\operatorname{rank}_{\mathbb C}(\rho)=k$ , and $k<n:=d_1d_2$ . Write $\beta(i,j)=id_2+j$ , and flatten a product-indexed matrix by $F(\sigma)_{u,v}=\sigma_{\beta^{-1}(u),\beta^{-1}(v)}$ . For every permutation $p$ of $\{0,\ldots,n-1\}$ , every complex $k\times(n-k)$ matrix $A$ , and every positive definite complex $k\times k$ matrix $K$ , assume

F(\rho)_{p(u),p(v)} = \begin{pmatrix} K&KA\\ A^*K&A^*KA \end{pmatrix}_{u,v},

where the blocks use the first $k$ and last $n-k$ coordinates and $^{*}$ denotes conjugate transpose. For each complex $k\times k$ matrix $L$ , define a product-indexed matrix $\Delta_L$ by

(\Delta_L)_{a,b} = \begin{pmatrix} L&LA\\ A^*L&A^*LA \end{pmatrix}_{p^{-1}(\beta(a)),\,p^{-1}(\beta(b))}.

Assume that every Hermitian $L$ for which both partial traces vanish,

\sum_j(\Delta_L)_{(i,j),(i',j)}=0\quad\text{for all }i,i', \qquad \sum_i(\Delta_L)_{(i,j),(i,j')}=0\quad\text{for all }j,j',

equals zero. Then $\rho$ is an extreme point of $C$ over the real numbers. The hypotheses exclude full rank; they also rule out $k=0$ and zero marginal dimensions because $\rho,\rho_1,\rho_2$ have trace $1$ .

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