Theorem 7: sufficient pure-state conversion condition

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.sufficient_pureConversion

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

prove2quantum

All Hilbert spaces are finite-dimensional complex spaces with fixed product bases and positive local dimensions. States are positive semidefinite operators of trace one; pure kets have norm one. A non-entangling map is completely positive and preserves the full separable positive cone. A channel is also trace preserving. Let $\psi$ and $\varphi$ be bipartite pure states, possibly on different registers, and let $\lambda_1>0$ be the largest squared Schmidt coefficient of $\psi$ . For standard robustness $R$ , if

1+R(\varphi)\le\frac1{\lambda_1},

then there exists a non-entangling channel $\Lambda$ such that $\Lambda(\psi)=\varphi$ .

This is a sufficient condition for exact conversion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P19

Formal statement

noncomputable section

open QAlgorithms QAlgorithms.Entanglement Filter

open scoped Matrix ComplexOrder ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P19

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P19 (Bip)

open QAlgorithms.Papers.Independent.Information100.P69 (CP)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower SupportIncluded)

open QAlgorithms.Papers.Independent.Dependency50.P19 (epr)

/-- Theorem 7, PDF p.11: a sufficient conversion criterion. The denominator
is positive for every unit ket; the conclusion is not an equivalence. -/
theorem sufficient_pureConversion {a b c d : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d)
    (psi : UnitBipartiteKet a b) (phi : UnitBipartiteKet c d)
    (hcriterion : 1 + standardStateRobustness phi.rho ≤ 1 / schmidtAt psi.ket 0) :
    ∃ L : Superop (Fin a × Fin b) (Fin c × Fin d),
      IsChannel L ∧ NE L ∧ L psi.rho = phi.rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 11, Theorem 7

Read-back

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

For all positive natural numbers $a,b,c,d$ and unit vectors $\psi\in\mathbb C^a\otimes\mathbb C^b$ and $\phi\in\mathbb C^c\otimes\mathbb C^d$ , let $P_\psi=|\psi\rangle\langle\psi|$ , $P_\phi=|\phi\rangle\langle\phi|$ , and let $\lambda_0(\psi)$ be the largest eigenvalue of the marginal matrix $(\sum_j\psi_{ij}\overline{\psi_{i'j}})_{i,i'}$ . Define $R_{\mathrm s}(\rho)$ as the real infimum of all $s\ge0$ for which there is a separable density matrix $\sigma$ such that $\rho+s\sigma$ is separable positive. “Separable positive” means a finite nonnegative sum of tensor products of positive semidefinite trace-one matrices, with the empty sum allowed, and a separable density matrix additionally is positive semidefinite of trace $1$ . If $1+R_{\mathrm s}(P_\phi)\le 1/\lambda_0(\psi)$ , then there exists a map $L$ with $L(P_\psi)=P_\phi$ that is a channel and is non-entangling. Explicitly, $L$ has a finite Kraus representation $L(X)=\sum_jE_jXE_j^\dagger$ valid for every operator $X$ , with $\sum_jE_j^\dagger E_j=I$ , and it maps every separable positive input to a separable positive output; the non-entangling condition also includes the existence of a finite Kraus representation without a normalization requirement. No lower bound greater than $1$ is imposed on any of the four dimensions.

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