An E_W/E_eta gap guarantees PPT and LOCC irreversibility

Open

QAlgorithms.Papers.Independent.Intakethird100.P90.wang_duan_irreversibility_criterion

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

prove2quantum

All systems are finite-dimensional complex Hilbert spaces with fixed orthonormal product bases and positive local dimensions. A state is a positive semidefinite operator of trace one. All logarithms are base two and all operational rates are measured in standard Bell pairs (ebits) per input copy, with deterministic operations and error tending to zero. Write $E_D,E_C$ for distillable entanglement and entanglement cost under completely PPT-preserving CPTP operations; an explicit LOCC subscript denotes unrestricted two-way local operations and classical communication.

For a bipartite state $\rho$ with support projection $P$ , put $E_W(\rho)=\inf_{X=X^\dagger,\,X\ge\rho}\log_2\|X^{T_B}\|_1$ and $E_\eta(\rho)=-\log_2\min\{\|Y^{T_B}\|_\infty:Y=Y^\dagger,\ -Y\le P^{T_B}\le Y\}$ . If $E_W(\rho)<E_\eta(\rho)$ , then

E_D(\rho)<E_C(\rho),\qquad E_{D,\mathrm{LOCC}}(\rho)<E_{C,\mathrm{LOCC}}(\rho).

The paper credits the background upper bound $E_D\le E_W$ to Ref. [30]. The additional LOCC conclusion is explicitly advertised in the abstract and discussion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P90

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P90

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms

open QAlgorithms.Papers.Independent.Dependency50.P36
  (relativeEntropy rains target canonicalMatrix allowed pptDistillable)

open QAlgorithms.Papers.Independent.Information100.P04 (gamma copies IsPPT)

open QAlgorithms.Papers.Independent.Next46.P42 (regroupProduct)

open QAlgorithms.Papers.Independent.Information100.P06 (supportProjection)

open QAlgorithms.Papers.Independent.Information100.P21 (FiniteLOCC)

open QAlgorithms.Papers.Independent.Gap48.P32 (antisymmetricQutrit)

/-- arXiv:1606.09421v3, PDF pp.4--5: the displayed PPT criterion and its
explicitly advertised LOCC consequence. E_D<=E_W is credited to Ref.[30]. -/
theorem wang_duan_irreversibility_criterion {A B : Type} [Fintype A] [Fintype B]
    [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hstate : IsDensityMatrix rho)
    (hgap : wangDuanBound rho < etaEntanglement rho) :
    pptDistillable rho < asymptoticEntanglementCost false rho ∧
    loccDistillable rho < asymptoticEntanglementCost true rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P90

end

Source

Irreversibility of Asymptotic Entanglement Manipulation Under Quantum Operations Completely Preserving Positivity of Partial Transpose, arXiv:1606.09421v3, PDF p. 4, Unnumbered sufficient condition: E_W below E_eta forces irreversibility

Read-back

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

For arbitrary finite, nonempty types $A,B$ , both equipped with decidable equality, and every complex matrix $\rho$ on $A\times B$ , assume that $\rho\ge0$ , $\operatorname{Tr}\rho=1$ , and $W(\rho)<\eta(\rho)$ , where, writing $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ ,

W(\rho)=\inf_{\substack{X=X^\dagger\\X-\rho\ge0}}\log_2\|\Gamma X\|_1, \qquad \eta(\rho)=-\log_2 \inf_{\substack{Y=Y^\dagger\\Y-\Gamma P_\rho\ge0\\Y+\Gamma P_\rho\ge0}}\|\Gamma Y\|_{\rm op}.

Here $P_\rho$ is obtained from $\rho$ by spectral functional calculus for the function equal to $0$ at $0$ and $1$ elsewhere, $\|\cdot\|_{\rm op}$ is the Euclidean operator norm, $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , and $\log_2x=\log x/\log2$ uses the total real logarithm with $\log0=0$ . The conclusion is

D_{\mathrm{PPT}}(\rho)<C_{\mathrm{PPT}}(\rho), \qquad D_{\mathrm{LOCC}}(\rho)<C_{\mathrm{LOCC}}(\rho)

in the extended real line. A channel is a finite Kraus sum $X\mapsto\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ ; PPT channels are those whose input-output partial-transpose conjugates are also channels. Finite LOCC maps are generated by the identity and finite recursive trees of complete local Kraus instruments on either party, with outcome-dependent subsequent maps and all branches summed. Let $\Phi_k$ have entry $1/k$ when both row and column have equal party indices and $0$ otherwise, and let $\widehat{\rho^{\otimes n}}$ denote the matrix with product entries, grouped by party and relabelled by fixed bijections with finite initial segments. The quantity $D_{\mathrm{PPT}}(\rho)$ is the supremum of real $r\ge0$ such that, for every $\varepsilon>0$ , all sufficiently large natural $n$ admit a PPT map with $\|\Lambda(\widehat{\rho^{\otimes n}})-\Phi_{\lceil2^{nr}\rceil}\|_1\le\varepsilon$ . The quantity $D_{\mathrm{LOCC}}(\rho)$ is the supremum of real $r\ge0$ such that, for every $\varepsilon,\delta>0$ , all sufficiently large positive natural $n$ admit $m\in\mathbb N$ and a finite LOCC map with $n(r-\delta)\le m$ and $\|\Lambda(\widehat{\rho^{\otimes n}})-\Phi_{2^m}\|_1\le\varepsilon$ . For either class $\mathcal C$ , $C_{\mathcal C}(\rho)$ is the infimum of real $r\ge0$ such that, for every $\varepsilon,\delta>0$ , all sufficiently large positive natural $n$ admit $m\in\mathbb N$ and $\Lambda\in\mathcal C$ with $m\le n(r+\delta)$ and $\|\Lambda(\Phi_{2^m})-\widehat{\rho^{\otimes n}}\|_1\le\varepsilon$ . These definitions allow $m=0$ and one-dimensional party types.

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