Abstract and Section IV: PPT catalysis exists with a maximally entangled catalyst

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.pptCatalysis

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

prove2quantum

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 positive integer $K$ , $\Phi_K$ denotes the maximally entangled state of Schmidt rank $K$ . There exists a strictly positive three-entry probability vector $\lambda$ for which

\Phi_2\not\to^{\rm PPT}\rho_\lambda,\qquad\exists C\ge2:\;\Phi_C\otimes\Phi_2\to^{\rm PPT}\Phi_C\otimes\rho_\lambda.

Hence PPT catalysis occurs even when the catalyst is maximally entangled, as asserted in the abstract and Section IV.

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.1,9–10: PPT catalysis exists, even with a maximally entangled catalyst.
Figure 1 and the strict inclusion following (51) identify an EPR input and rank-three target. -/
theorem pptCatalysis :
    ∃ lam : Fin 3 → ℝ, IsProbability lam ∧ (∀ i, 0 < lam i) ∧
      ¬ Reach (maximallyEntangledDensity 2) (schmidtDensity lam) ∧ CatalyticPreparation 2 lam := 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. 1, Abstract and Section IV: PPT catalysis exists with a maximally entangled catalyst

Read-back

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

There exists a vector $\lambda=(\lambda_0,\lambda_1,\lambda_2)$ with $\lambda_i>0$ and $\lambda_0+\lambda_1+\lambda_2=1$ for which no complex-linear, trace-preserving map $\mathcal L$ sends $\Omega_2$ to $\rho_\lambda$ while making both $\mathcal L$ and $\Gamma_{\rm out}\mathcal L\Gamma_{\rm in}$ completely positive, but for which there exist an integer $C\ge2$ and such a map sending $\Omega_C\otimes\Omega_2$ to $\Omega_C\otimes\rho_\lambda$ . Here $\Omega_m=m^{-1}\sum_{i,j=0}^{m-1}|ii\rangle\langle jj|$ , and $\rho_\lambda$ has entries $\sqrt{\lambda_i\lambda_k}$ at $((i,i),(k,k))$ and zero elsewhere. The tensor products group each party’s two factors together, and $\Gamma$ transposes the second party’s factor, $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ . Trace preservation holds for every matrix, and complete positivity requires positivity preservation after every finite identity amplification, including size zero. No ordering of the three entries is required.

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