Abstract and Conjecture 19: conditional full preparation criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.conditionalCharacterization

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 $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$ . Write $T_1(K;\lambda)$ for the supremum of the dual objective (28) over feasible coordinates whose associated matrix has rank exactly one; attainment is not assumed. Suppose, as a premise rather than a proved claim, that $T(K;\lambda)=T_1(K;\lambda)$ for every $K\ge2$ and every strictly positive finite probability vector. Then for every such instance,

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

This states the abstract’s full preparation criterion conditionally on the optimal-value equality implied by Conjecture 19.

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,5,8: the abstract's conditional criterion. The premise is explicitly
the conjectured equality of values (Conjecture 19's consequence), not a proved fact. -/
theorem conditionalCharacterization
    (hconjecture : ∀ (d K : ℕ), 2 ≤ K → ∀ lam : Fin d → ℝ,
      IsProbability lam → (∀ i, 0 < lam i) → primalValue K lam = rankOneValue K lam)
    {d : ℕ} (K : ℕ) (hK : 2 ≤ K) (lam : Fin d → ℝ)
    (hprob : IsProbability lam) (hpos : ∀ i, 0 < lam i) :
    Reach (maximallyEntangledDensity K) (schmidtDensity lam) ↔ rankOneValue 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. 1, Abstract and Conjecture 19: conditional full preparation criterion

Read-back

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

For a vector $\lambda\in\mathbb R^d$ , define $R_\lambda=(\sum_i\sqrt{\lambda_i})^2$ and $B_K(\lambda)=(K R_\lambda-1)/(K^2-1)$ . Define $S_{ii}=|ii\rangle\langle ii|$ , $S_{ij}=\frac12(|ij\rangle+|ji\rangle)(\langle ij|+\langle ji|)$ and $A_{ij}=\frac12(|ij\rangle-|ji\rangle)(\langle ij|-\langle ji|)$ for $j<i$ , on $\mathbb C^d\otimes\mathbb C^d$ , and set $Q(s,a)=\sum_{j\le i}s_{ij}\Gamma S_{ij}+\sum_{j<i}a_{ij}\Gamma A_{ij}$ , where $(\Gamma X)_{(i,j),(k,l)}=X_{(i,l),(k,j)}$ . Let $V_K(\lambda)$ be the real infimum of $\sum_{j\le i}s_{ij}+\sum_{j<i}a_{ij}$ subject to $Q(s,a)\succeq0$ , $s_{ij}\ge\sqrt{\lambda_i\lambda_j}/(K+1)$ , and $a_{ij}\ge\sqrt{\lambda_i\lambda_j}/(K-1)$ . Let $W_K(\lambda)$ be the real supremum of

B_K(\lambda)-\sum_{j\le i}\frac{\mu_{ij}\sqrt{\lambda_i\lambda_j}}{K+1} -\sum_{j<i}\frac{t_{ij}\sqrt{\lambda_i\lambda_j}}{K-1}

subject to the real coefficient bounds $\mu_{ij}\le1$ , $t_{ij}\le1$ , positive semidefiniteness of $Q(\mu,t)$ , and $\operatorname{rank}Q(\mu,t)=1$ . Assume that $V_K(\lambda)=W_K(\lambda)$ for every pair of natural numbers $d,K$ with $K\ge2$ and every strictly positive probability vector $\lambda\in\mathbb R^d$ . Under this assumption, for every natural $d$ , every $K\ge2$ , and every $\lambda_i>0$ with $\sum_i\lambda_i=1$ , there exists a complex-linear, trace-preserving map $\mathcal L$ such that $\mathcal L$ and $\Gamma_{\rm out}\mathcal L\Gamma_{\rm in}$ are completely positive and $\mathcal L(\Omega_K)=\rho_\lambda$ if and only if $W_K(\lambda)\le1$ . Here $\Omega_K=K^{-1}\sum_{i,j}|ii\rangle\langle jj|$ , and $\rho_\lambda$ has entries $\sqrt{\lambda_i\lambda_k}$ at $((i,i),(k,k))$ and zero elsewhere; complete positivity requires positivity preservation under every finite identity amplification, including size zero. The probability hypotheses exclude $d=0$ , and neither ordering of $\lambda$ nor a relation between $K$ and $d$ is assumed.

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