Explicit single-copy PPT channel with fidelity above the distillation threshold

Open

QAlgorithms.Papers.Independent.Intakethird100.P43.single_copy_fidelity

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$ , $m\ge2$ , and let $\rho$ be an NPT density operator. Let $P_{\rm neg}$ be the spectral projector of $\rho^\Gamma$ on its strictly negative eigenvalues, and let $\mathcal N(\rho)$ be the sum of their absolute values. The norm $\|\cdot\|_\infty$ is the operator norm. For

0<\epsilon\le\min\{2,\|P_{\rm neg}^\Gamma\|_\infty^{-1}\},\qquad A=\frac{I-\epsilon P_{\rm neg}^\Gamma}{m},

$A$ satisfies the isotropic admissibility constraints, and its channel $T_A$ , defined by the two-coefficient formula with $B=(I-A)/(m^2-1)$ , satisfies

\operatorname{tr}(\rho A)=\operatorname{tr}(P_mT_A(\rho))=\frac{1+\epsilon\mathcal N(\rho)}m>\frac1m.

This is the constructive single-copy threshold witness; it does not claim single-copy perfect distillation.

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, (6)–(7): the explicit single-copy witness, its admissibility and its
channel fidelity, strictly above 1/m. Negativity reuses the frozen first-party scalar;
first- and second-party partial transposes are full transposes and have equal trace norms.
NPT makes P_neg nonzero and the operator-norm reciprocal in the interval nondegenerate. -/
theorem single_copy_fidelity (d m : ℕ) (hd : 0 < d) (hm : 2 ≤ m)
    (rho : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ)
    (hrho : IsDensityMatrix rho) (hnpt : ¬ (gamma rho).PosSemidef)
    (epsilon : ℝ) (hepsilon : 0 < epsilon)
    (hbound : epsilon ≤ min (2 : ℝ) ((specNorm (gamma (negativeProjector rho)))⁻¹)) :
    let A := negativeSpaceWitness rho m epsilon
    RainsFeasibleEffect m A ∧ IsPositiveConjugatePPTChannel (isotropicPreparation m A) ∧
      effectProb A rho = (1 + epsilon * Entanglement.negativity rho) / (m : ℝ) ∧
      effectProb (bellProjector m) (isotropicPreparation m A rho) = (1 + epsilon * Entanglement.negativity rho) / (m : ℝ) ∧
      1 / (m : ℝ) < effectProb (bellProjector m) (isotropicPreparation m A 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 proof, Eqs. (6)–(7)

Read-back

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

For every pair of natural numbers $d>0$ and $m\ge2$ , every complex matrix $\rho$ indexed by $\{0,\ldots,d-1\}^2$ that is positive semidefinite with trace one, and every real $\epsilon>0$ , define $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ and suppose that $\Gamma\rho$ is not positive semidefinite and

\epsilon\le\min\!\left\{2,\frac1{\|\Gamma Q\|_{\mathrm{op}}}\right\}, \qquad Q=\mathbf1_{(-\infty,0)}(\Gamma\rho),

where $Q$ is obtained by applying the function that is one on negative eigenvalues and zero elsewhere through the continuous functional calculus. Set $A=(I-\epsilon\Gamma Q)/m$ , let $P_m$ have entry $1/m$ when both row and column pairs have equal components and zero otherwise, and define

\mathcal P_m(A)(X) =\frac{\operatorname{tr}(X(I-A))}{m^2-1}(I-P_m)+\operatorname{tr}(XA)P_m.

Then $A$ is Hermitian and $A$ , $I-A$ , $I-m\Gamma A$ , and $I+m\Gamma A$ are positive semidefinite. The map $\mathcal P_m(A)$ is positive and trace preserving, satisfies $\Gamma\mathcal P_m(A)(\Gamma X)\ge0$ for every $X\ge0$ , and is completely positive, meaning that its blockwise extension by an identity map preserves positivity for every finite auxiliary size, including zero. Furthermore,

\operatorname{Re}\operatorname{tr}(A\rho) =\operatorname{Re}\operatorname{tr}\!\bigl(P_m\mathcal P_m(A)(\rho)\bigr) =\frac{1+\epsilon N}{m}, \qquad \frac1m<\operatorname{Re}\operatorname{tr}\!\bigl(P_m\mathcal P_m(A)(\rho)\bigr),

where $N=(\|\Gamma_1\rho\|_1-1)/2$ , $(\Gamma_1X)_{(a,b),(a',b')}=X_{(a',b),(a,b')}$ , and $\|Y\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Y^\dagger Y}$ . The norm $\|\cdot\|_{\mathrm{op}}$ is the Euclidean operator norm; its reciprocal in the hypothesis is defined to be zero if the norm is zero, in which case no positive $\epsilon$ satisfies the 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