Theorem 18: exact rank-three preparation from an EPR pair

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.theorem18

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$ . Assume that $\lambda$ has exactly three strictly positive entries, ordered as $\lambda_1^\uparrow\le\lambda_2^\uparrow\le\lambda_3^\uparrow$ . Then

\Phi_2\to^{\rm PPT}\rho_\lambda\quad\Longleftrightarrow\quad2\bigl(\sqrt{\lambda_3^\uparrow\lambda_2^\uparrow}+\sqrt{\lambda_3^\uparrow\lambda_1^\uparrow}\bigr)+4\sqrt{\lambda_1^\uparrow\lambda_2^\uparrow}\le1.

This is the exact rank-three preparation criterion from one EPR pair.

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.8, Theorem 18, (47): ordered Schmidt probabilities, coefficients 2,2,4. -/
theorem theorem18 (lam : Fin 3 → ℝ) (hprob : IsProbability lam)
    (hpos : ∀ i, 0 < lam i) (hsorted : Monotone lam) :
    Reach (maximallyEntangledDensity 2) (schmidtDensity lam) ↔
      2 * (Real.sqrt (lam 2 * lam 1) + Real.sqrt (lam 2 * lam 0)) +
        4 * Real.sqrt (lam 0 * lam 1) ≤ 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. 8, Theorem 18: exact rank-three preparation from an EPR pair

Read-back

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

For every probability vector $\lambda=(\lambda_0,\lambda_1,\lambda_2)$ satisfying $0<\lambda_0\le\lambda_1\le\lambda_2$ and $\lambda_0+\lambda_1+\lambda_2=1$ , let $\Omega_2=\frac12\sum_{i,j=0}^1|ii\rangle\langle jj|$ , and let $\rho_\lambda$ on $\mathbb C^3\otimes\mathbb C^3$ have entry $\sqrt{\lambda_i\lambda_k}$ at $((i,i),(k,k))$ and zero entries elsewhere. There exists a complex-linear, trace-preserving, completely positive map $\mathcal L$ with $\mathcal L(\Omega_2)=\rho_\lambda$ and with $\Gamma_{\rm out}\mathcal L\Gamma_{\rm in}$ completely positive if and only if

2\bigl(\sqrt{\lambda_2\lambda_1}+\sqrt{\lambda_2\lambda_0}\bigr) +4\sqrt{\lambda_0\lambda_1}\le1.

Here $\Gamma$ is partial transpose on the second tensor factor, $(\Gamma X)_{(i,j),(k,l)}=X_{(i,l),(k,j)}$ ; trace preservation applies to every matrix, and complete positivity requires positivity preservation after every finite identity amplification, including size zero.

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