Proposition 4: exact PPT distillable entanglement

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.proposition4

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

prove2quantum

Let $\lambda=(\lambda_1,\ldots,\lambda_d)$ be a finite probability vector: every entry is nonnegative and the entries sum to one. Write $\rho_\lambda=\sum_{i,j}\sqrt{\lambda_i\lambda_j}|ii\rangle\langle jj|$ . All logarithms have base two. A PPT operation is a completely positive, trace-preserving map $L$ such that $\Gamma_{\rm out}L\Gamma_{\rm in}$ is completely positive for arbitrary finite ancillary systems; $\Gamma$ transposes Bob in the fixed product basis. For a finite order $t$ , $S_t$ is the Rényi entropy, with $S_0$ the log support size, $S_1=-\sum_i\lambda_i\log_2\lambda_i$ (using $0\log_2 0=0$ ), and $S_t=(1-t)^{-1}\log_2\sum_i\lambda_i^t$ otherwise. The separate infinity order is $S_\infty=-\log_2\max_i\lambda_i$ . The exact PPT distillable entanglement $E_{xd}$ is the supremum of limiting normalized log output ranks of PPT distillation protocols with positive block lengths tending to infinity and zero error at every block. Rank-one output represents rate zero. Then

E_{xd}^{\rm PPT}(\rho_\lambda)=S_\infty(\lambda).

This distinguishes exact asymptotic concentration from concentration with vanishing error.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P95

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P95

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact primitives from the pinned accepted library; no local aliases.

open QAlgorithms.Papers.Independent.Claimed50.P28 (maximallyEntangledDensity)

open QAlgorithms.Papers.Independent.Information100.P27 (IsProbability)

open QAlgorithms.Papers.Independent.Information100.P63 (logTwo)

open QAlgorithms.Papers.Independent.Information100.P19 (outer)

open QAlgorithms.Papers.Independent.Dependency50.P18 (bipartiteTensor)

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

/-- PDF pp.3–4, Proposition 4: exact distillation, not vanishing-error distillation. -/
theorem proposition4 {d : ℕ} (lam : Fin d → ℝ) (hprob : IsProbability lam) :
    pptDistillableEntanglement lam true = (renyiInfinity lam : EReal) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P95

end

Source

Pure-state transformations and catalysis under operations that completely preserve positivity of partial transpose, arXiv:0801.4322v2, PDF p. 3, Proposition 4: exact PPT distillable entanglement

Read-back

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

Let $d$ be any natural number and let $\lambda=(\lambda_i)_{i=0}^{d-1}$ have nonnegative entries summing to one, which excludes $d=0$ . Define $\rho_\lambda=|\psi_\lambda\rangle\langle\psi_\lambda|$ by $\psi_\lambda=\sum_i\sqrt{\lambda_i}\,|i,i\rangle$ , and define $\Omega_K=K^{-1}\sum_{i,j=0}^{K-1}|i,i\rangle\langle j,j|$ for positive $K$ . Consider all real numbers $R$ for which there exist sequences of positive integers $n_j,K_j$ , with $n_j\to\infty$ and $\log_2K_j/n_j\to R$ , and complex-linear, trace-preserving, completely positive maps taking $\rho_\lambda^{\otimes n_j}$ exactly to $\Omega_{K_j}$ for every $j$ , such that partial transposition on the second subsystem before and after each map also gives a completely positive map. Complete positivity requires positivity preservation after amplification by every finite-dimensional identity map, including dimension zero. The supremum of these rates in the extended real numbers is

\operatorname{pptDistillableEntanglement}(\lambda,\mathrm{true}) =-\log_2\!\left(\max_i\lambda_i\right),

where $\log_2x=\log x/\log2$ and the right-hand side is embedded into the extended reals. Zero entries of $\lambda$ are allowed.

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