Proposition 5: exact PPT pure-state entanglement cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.proposition5

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 formation cost $E_{xc}$ is the infimum of limiting normalized log input ranks for PPT protocols that prepare every block exactly, with positive block lengths tending to infinity. Then

E_{xc}^{\rm PPT}(\rho_\lambda)=S_{1/2}(\lambda).

The paper obtains this pure-state formula as an application of Audenaert–Plenio–Eisert [4].

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 p.4, Proposition 5: EXACT formation cost, an application of Audenaert–Plenio–Eisert [4]. -/
theorem proposition5 {d : ℕ} (lam : Fin d → ℝ) (hprob : IsProbability lam) :
    pptEntanglementCost lam true = (schmidtRenyi (1 / 2) 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. 4, Proposition 5: exact PPT pure-state entanglement cost

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, so $d=0$ cannot satisfy the hypotheses. Define $\rho_\lambda=|\psi_\lambda\rangle\langle\psi_\lambda|$ with $\psi_\lambda=\sum_i\sqrt{\lambda_i}\,|i,i\rangle$ , and $\Omega_K=K^{-1}\sum_{i,j=0}^{K-1}|i,i\rangle\langle j,j|$ for positive $K$ . Consider all real rates $R$ admitting 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 that take $\Omega_{K_j}$ exactly to $\rho_\lambda^{\otimes n_j}$ for every $j$ and remain completely positive after partial transposition on the second subsystem before and after the map. Complete positivity here requires positivity preservation under every finite-dimensional identity amplification, including dimension zero. The infimum of these rates in the extended real numbers equals

\operatorname{pptEntanglementCost}(\lambda,\mathrm{true}) =2\log_2\!\left(\sum_i\sqrt{\lambda_i}\right),

with the real expression on the right embedded into the extended reals and $\log_2x=\log x/\log2$ . The entries of $\lambda$ need not all be positive.

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