Every NPT state is distillable via PPT-preserving channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P43.npt_distillable

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

prove2quantum

All operators act on a finite bipartite space $\mathbb C^d\otimes\mathbb C^d$ in a fixed product basis. Write $\Gamma=T_2$ for Bob's partial transpose and $P_m=|\psi_m\rangle\langle\psi_m|$ , where $|\psi_m\rangle=m^{-1/2}\sum_i|ii\rangle$ . A density operator is positive semidefinite with complex trace exactly one. An admissible PPT map is complex-linear, positive and trace preserving, and $\Gamma_{\rm out}T\Gamma_{\rm in}$ is positive on every positive operator. A PPT channel is additionally completely positive; complete positivity of the transpose-conjugated map is not required. Fidelity means the overlap $\operatorname{tr}(P_m T(\rho))$ .

Let $d\ge1$ and let $\rho$ be a density operator with $\rho^\Gamma\not\ge0$ . Then for every $0<\eta<1$ there are a positive integer $n$ and a PPT channel $T$ from $n$ copies to two qubits such that

\operatorname{tr}\!\left(P_2 T(\rho^{\otimes n})\right)\ge1-\eta.

The copies are grouped as Alice's registers versus Bob's registers. This is qualitative distillability with vanishing singlet error; no rate is specified.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P43

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P43

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Information100.P04
  (gamma copies bellProjector negativeProjector werner)

open QAlgorithms.Papers.Independent.Information100.P30 (IsPositiveMap)

/-- PDF p.2, Theorem 1 (abstract p.1; conclusion p.3): all finite-dimensional NPT
states are distillable through PPT-preserving channels, in the qualitative many-copy sense.
The single-copy threshold witness is stated separately and is not substituted for this goal. -/
theorem npt_distillable (d : ℕ) (hd : 0 < d)
    (rho : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ)
    (hrho : IsDensityMatrix rho) (hnpt : ¬ (gamma rho).PosSemidef) :
    IsPositiveConjugatePPTDistillable rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P43

end

Source

Distillability via protocols respecting the positivity of partial transpose, arXiv:quant-ph/0104095v2, PDF p. 2, Theorem 1

Read-back

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

For every natural number $d>0$ and every positive semidefinite complex matrix $\rho$ of trace one indexed by $\{0,\ldots,d-1\}^2$ , assume that $\Gamma(\rho)$ is not positive semidefinite, where $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ . Then for every real $\eta$ with $0<\eta<1$ , there exist a positive natural number $n$ and a complex-linear map $T$ from matrices on $\{0,\ldots,d-1\}^n\times\{0,\ldots,d-1\}^n$ to matrices on $\{0,1\}^2$ such that $T$ preserves positive semidefiniteness, preserves the trace of every matrix, satisfies $\Gamma(T(\Gamma(X)))\succeq0$ whenever $X\succeq0$ , and is completely positive, meaning that applying $T$ to each matrix block of any positive semidefinite matrix with any finite ancillary index set $\{0,\ldots,r-1\}$ , including $r=0$ , preserves positive semidefiniteness. These choices satisfy

1-\eta\le \operatorname{Re}\operatorname{tr}\!\left(B_2T(\rho^{[n]})\right), \qquad (\rho^{[n]})_{(a,b),(a',b')}= \prod_{t=0}^{n-1}\rho_{(a_t,b_t),(a'_t,b'_t)},

where $B_2$ has entry $\tfrac12$ when both its row pair and its column pair have equal components, and zero otherwise. The allowed case $d=1$ has no matrix satisfying the non-positive-partial-transpose hypothesis.

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