Theorem 21: maximally entangled PPT catalysts, seed headline

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.theorem21

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 positive integer $K$ , $\Phi_K$ denotes the maximally entangled state of Schmidt rank $K$ . 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$ . Let $K\ge2$ and assume the nonzero spectrum of $\lambda$ is not the uniform spectrum of rank $K$ . A maximally entangled catalyst of some finite rank $C\ge2$ exists exactly when

\bigl[\exists C\ge2:\;\Phi_C\otimes\Phi_K\to^{\rm PPT}\Phi_C\otimes\rho_\lambda\bigr]\quad\Longleftrightarrow\quad S_{1/2}(\lambda)<\log_2 K.

The catalyst is returned exactly and uncorrelated with the target, with tensor factors grouped by Alice and Bob. Its rank and the channel may depend on $K$ and $\lambda$ . This includes nontrivial targets of rank at most $K$ .

Furthermore, whenever $S_{1/2}(\lambda)<\log_2 K$ , there is an integer $C_0\ge2$ , depending only on $K$ and $\lambda$ , such that for every integer $C\ge C_0$ a PPT channel sends $\Phi_C\otimes\Phi_K$ exactly to $\Phi_C\otimes\rho_\lambda$ .

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.9, Theorem 21 (abstract pp.1–2): some finite maximally entangled catalyst
works iff S_{1/2}<log K, excluding the identical nonzero spectrum, up to local unitaries.
The catalyst is returned exactly in tensor product with the target. Below the
threshold, every sufficiently large finite catalyst rank works, as in the proof. -/
theorem theorem21 {d : ℕ} (K : ℕ) (hK : 2 ≤ K) (lam : Fin d → ℝ)
    (hprob : IsProbability lam) (hnontrivial : ¬ IsUniformRank lam K) :
    (CatalyticPreparation K lam ↔ schmidtRenyi (1 / 2) lam < logTwo (K : ℝ)) ∧
    (schmidtRenyi (1 / 2) lam < logTwo (K : ℝ) →
      ∃ C0 : ℕ, 2 ≤ C0 ∧ ∀ C : ℕ, C0 ≤ C →
        Reach (bipartiteTensor (maximallyEntangledDensity C) (maximallyEntangledDensity K))
          (bipartiteTensor (maximallyEntangledDensity C) (schmidtDensity 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. 9, Theorem 21: maximally entangled PPT catalysts, seed headline

Read-back

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

For every natural number $d$ , natural number $K\ge 2$ , and function $\lambda:\{0,\ldots,d-1\}\to\mathbb R$ satisfying $\lambda_i\ge0$ and $\sum_i\lambda_i=1$ , assume that it is not the case that exactly $K$ entries are nonzero and every entry is either $0$ or $1/K$ . (The probability assumptions cannot hold when $d=0$ .) Define $H_{1/2}(\lambda)=2\log_2(\sum_i\sqrt{\lambda_i})$ , where $\log_2 x=\log x/\log2$ ; define the bipartite matrix $\rho_\lambda$ by $(\rho_\lambda)_{(i,j),(i',j')}=\sqrt{\lambda_i\lambda_{i'}}$ when $i=j$ and $i'=j'$ , and zero otherwise; and define $\Gamma_m$ by $(\Gamma_m)_{(i,j),(i',j')}=1/m$ under the same equality conditions, and zero otherwise. Here the bipartite tensor product groups the two left factors together and the two right factors together: $(X\otimes_{\mathrm{bip}}Y)_{(a,c;\,b,e),(a',c';\,b',e')}=X_{(a,b),(a',b')}Y_{(c,e),(c',e')}$ . An allowed conversion means that there exists a complex-linear map taking the specified input matrix exactly to the specified output matrix, preserving the trace of every matrix, and such that both the map and its composition with partial transpose on the right subsystem before and after the map are completely positive; complete positivity requires preservation of positive semidefiniteness under every finite identity amplification, including amplification dimension zero. Then an allowed conversion

\Gamma_C\otimes_{\mathrm{bip}}\Gamma_K \longmapsto \Gamma_C\otimes_{\mathrm{bip}}\rho_\lambda

exists for some natural number $C\ge2$ if and only if $H_{1/2}(\lambda)<\log_2K$ . Moreover, if this strict inequality holds, there exists a natural number $C_0\ge2$ such that such an allowed conversion exists for every natural number $C\ge C_0$ , with the converting map permitted to depend on $C$ .

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