Lemma 8: general-state PPT preparation SDP

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.lemma8

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$ . Let $\rho$ be any density operator on any nonempty finite-dimensional product space $\mathcal H_A\otimes\mathcal H_B$ , allowing unequal local dimensions, mixed states, and zero eigenvalues. For $K\ge2$ , the following minimum is attained:

v=\min\{\operatorname{Tr}P:P=P^\dagger\ge0,\;-(K-1)P^\Gamma\le\rho^\Gamma\le(K+1)P^\Gamma\}.

Then $\Phi_K\to^{\rm PPT}\rho$ if and only if $v\le1$ . All matrix inequalities are Loewner inequalities and use the same $P$ .

This is the general finite-dimensional preparation SDP.

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.5, Lemma 8: arbitrary mixed or pure state, arbitrary rectangular local dimensions.
IsLeast preserves the source's minimum and rules out default real infima. -/
theorem lemma8 {A B : Type*} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B]
    (K : ℕ) (hK : 2 ≤ K) (X : Matrix (A × B) (A × B) ℂ)
    (hstate : QAlgorithms.IsDensityMatrix X) :
    IsLeast (preparationValues K X) (preparationValue K X) ∧
      (Reach (maximallyEntangledDensity K) X ↔ preparationValue K X ≤ 1) := 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. 5, Lemma 8: general-state PPT preparation SDP

Read-back

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

Let $A,B$ be finite nonempty types, let $K\in\mathbb N$ satisfy $K\ge2$ , and let $X$ be a complex matrix indexed by $A\times B$ that is positive semidefinite with trace one. Write $\Gamma X$ for partial transposition on the second subsystem, so $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ . Let $\mathcal V_K(X)$ be the set of real numbers $\operatorname{Re}\operatorname{tr}P$ arising from Hermitian positive semidefinite matrices $P$ on $A\times B$ satisfying

\Gamma X+(K-1)\Gamma P\succeq0, \qquad (K+1)\Gamma P-\Gamma X\succeq0,

and put $v_K(X)=\inf\mathcal V_K(X)$ in $\mathbb R$ . Then $v_K(X)$ belongs to $\mathcal V_K(X)$ and is no greater than every member of that set. Moreover, $\Omega_K=K^{-1}\sum_{i,j<K}|i,i\rangle\langle j,j|$ can be mapped exactly to $X$ by a complex-linear, trace-preserving, completely positive map whose conjugation by partial transposition on the second subsystem is also completely positive if and only if $v_K(X)\le1$ . Complete positivity means preservation of positive semidefiniteness after every finite-dimensional identity amplification, including dimension zero. No positivity condition on $\Gamma P$ is separately imposed.

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