Proposition 9: Schmidt-coordinate primal SDP

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.proposition9

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. Assume in addition that all entries of $\lambda$ are strictly positive, so $d$ is its Schmidt rank. For a positive integer $K$ , $\Phi_K$ denotes the maximally entangled state of Schmidt rank $K$ . For $K\ge2$ , let $T(K;\lambda)$ be the minimum of the Schmidt-coordinate primal SDP (20), defined independently of operational reachability. Its real variables $s_{ij}$ for $j\le i$ and $a_{ij}$ for $j<i$ obey $s_{ij}\ge\sqrt{\lambda_i\lambda_j}/(K+1)$ and $a_{ij}\ge\sqrt{\lambda_i\lambda_j}/(K-1)$ , and the matrix $\sum_{i\ge j}s_{ij}\sigma_{ij}^{\Gamma}+\sum_{i>j}a_{ij}\alpha_{ij}^{\Gamma}$ is positive semidefinite. The objective is $\sum s_{ij}+\sum a_{ij}$ . Here $\sigma_{ii}=|ii\rangle\langle ii|$ , while the off-diagonal symmetric and antisymmetric projectors are $(|ij\rangle\pm|ji\rangle)(\langle ij|\pm\langle ji|)/2$ . The minimum is attained, and

\Phi_K\to^{\rm PPT}\rho_\lambda\quad\Longleftrightarrow\quad T(K;\lambda)\le1.

This translates pure-state preparation into Schmidt-coordinate semidefinite optimization.

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.5–6, Proposition 9: the primal minimum is attained and characterizes preparation. -/
theorem proposition9 {d : ℕ} (K : ℕ) (hK : 2 ≤ K) (lam : Fin d → ℝ)
    (hprob : IsProbability lam) (hpos : ∀ i, 0 < lam i) :
    IsLeast (primalValues K lam) (primalValue K lam) ∧
      (Reach (maximallyEntangledDensity K) (schmidtDensity lam) ↔ primalValue K lam ≤ 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, Proposition 9: Schmidt-coordinate primal SDP

Read-back

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

Let $d,K\in\mathbb N$ , with $K\ge2$ , and let $\lambda=(\lambda_i)_{i=0}^{d-1}$ satisfy $\lambda_i>0$ for every $i$ and $\sum_i\lambda_i=1$ ; thus $d=0$ is excluded. For $0\le j\le i<d$ , let $S_{ii}=|i,i\rangle\langle i,i|$ and, when $i\ne j$ , let $S_{ij}=\tfrac12(|i,j\rangle+|j,i\rangle)(\langle i,j|+\langle j,i|)$ ; for $0\le j<i<d$ , let $A_{ij}=\tfrac12(|i,j\rangle-|j,i\rangle)(\langle i,j|-\langle j,i|)$ . Write $\Gamma$ for partial transposition on the second subsystem and define

C(s,a)=\sum_{j\le i}s_{ij}\Gamma S_{ij} +\sum_{j<i}a_{ij}\Gamma A_{ij}.

Let $\mathcal P_K(\lambda)$ consist of the real values $\sum_{j\le i}s_{ij}+\sum_{j<i}a_{ij}$ for real coefficient families satisfying $s_{ij}\ge\sqrt{\lambda_i\lambda_j}/(K+1)$ , $a_{ij}\ge\sqrt{\lambda_i\lambda_j}/(K-1)$ , and $C(s,a)\succeq0$ , and put $p_K(\lambda)=\inf\mathcal P_K(\lambda)$ in $\mathbb R$ . Then $p_K(\lambda)$ belongs to this set and is no greater than every member. Furthermore, with $\rho_\lambda=|\sum_i\sqrt{\lambda_i}|i,i\rangle|^2$ understood as the outer product of that vector with itself and $\Omega_K=K^{-1}\sum_{u,v<K}|u,u\rangle\langle v,v|$ , there exists a complex-linear, trace-preserving, completely positive map taking $\Omega_K$ exactly to $\rho_\lambda$ and remaining completely positive after partial transposition on the second subsystem before and after the map if and only if $p_K(\lambda)\le1$ . Complete positivity includes every finite-dimensional identity amplification, and for $d=1$ the antisymmetric index set is empty.

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