Positivity detects PPT distillability

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.positivityDetectsDistillability

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

prove2quantum

Let $\rho$ be any normalized bipartite state on nonzero finite-dimensional complex spaces. Let $E_W$ be the logarithm of SDP (7), and define $E_\Gamma$ by the supremum of rates whose Eq. (3) distillation fidelity tends to one. Then

E_W(\rho)>0\quad\Longleftrightarrow\quad E_\Gamma(\rho)>0.

Moreover, $T_B(\rho)\ge0$ implies $E_W(\rho)=0$ . Thus positivity of this SDP measure detects positive-rate PPT distillability, including rank-deficient states.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P83

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P83

open QAlgorithms.Papers.Independent.Support50.P11 (Loewner)

open QAlgorithms.Papers.Independent.Dependency50.P32 (partialTranspose)

open QAlgorithms.Papers.Independent.Information100.P34 (supportProjector)

variable {A B C D : Type*}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

/-- Theorem 2 and its PPT-zero case, PDF p.3. The NPPT characterization
is a conclusion of the proof, not an extra hypothesis. -/
theorem positivityDetectsDistillability [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    (0 < entanglementW rho ↔ 0 < entanglementGamma rho) ∧
    ((partialTranspose rho).PosSemidef → entanglementW rho = 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 3, Theorem 2: positivity detects PPT distillability

Read-back

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

Let $A,B$ be finite nonempty types with decidable equality, and let $\rho$ be a positive semidefinite complex matrix on $A\times B$ with trace $1$ . Write $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , use $X\le Y$ to mean $Y-X\ge0$ , and define

W(\rho)=\log_2\sup\{\operatorname{Re}\operatorname{tr}(\rho^\Gamma R): R=R^\dagger,\ \|R\|_{\mathrm{op}}\le1,\ R^\Gamma\ge0\},

with the Euclidean operator norm. Define $F(X,k)$ as the supremum of $\operatorname{Re}\operatorname{tr}(XQ)$ over matrices $Q$ satisfying $k>0$ , $0\le Q\le I$ , and $-k^{-1}I\le Q^\Gamma\le k^{-1}I$ . For natural $n$ , define the matrix $\rho^{[n]}$ on $A^n\times B^n$ by taking the product of the corresponding $n$ entries of $\rho$ , with the empty product equal to $1$ . Put

\Gamma(\rho)=\sup\{r\in\mathbb R: F(\rho^{[n]},2^{nr})\longrightarrow1\text{ as }n\to\infty\}.

There is no separate nonnegativity requirement on rates in this supremum. The theorem asserts

W(\rho)>0\ \Longleftrightarrow\ \Gamma(\rho)>0, \qquad \rho^\Gamma\ge0\ \Longrightarrow\ W(\rho)=0.

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