Theorem 1: exact conversion from maximally entangled currency

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.maximallyEntangled_conversion

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 $k\ge2$ , let $\phi_k^+$ be the normalized maximally entangled state on $\mathbb C^k\otimes\mathbb C^k$ , and let $\psi$ be any bipartite pure output state, on possibly different local dimensions. Write $R(\rho)$ for the standard robustness, minimized over separable normalized noise. Then

\exists\,\Lambda\text{ non-entangling channel}:\Lambda(\phi_k^+)=\psi\quad\Longleftrightarrow\quad R(\psi)\le R(\phi_k^+).

This characterizes exact preparation from maximally entangled currency.

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 1, PDF p.8: exact conversion from maximally entangled currency
is characterized by standard robustness, with arbitrary positive output dimensions. -/
theorem maximallyEntangled_conversion {a b k : ℕ} (ha : 0 < a) (hb : 0 < b)
    (hk : 2 ≤ k) (psi : UnitBipartiteKet a b) :
    (∃ L : Superop (Fin k × Fin k) (Fin a × Fin b),
      IsChannel L ∧ NE L ∧ L (epr k) = psi.rho) ↔
      standardStateRobustness psi.rho ≤ standardStateRobustness (epr k) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 8, Theorem 1

Read-back

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

For all natural numbers $a,b,k$ with $a>0$ , $b>0$ , and $k\ge2$ , and every complex Euclidean vector $\psi$ on $\{0,\ldots,a-1\}\times\{0,\ldots,b-1\}$ satisfying $\|\psi\|=1$ , put $\rho_\psi=\psi\psi^\dagger$ . Call a matrix separable positive if it is a finite sum $\sum_iw_iA_i\otimes B_i$ , where $w_i\ge0$ and each $A_i,B_i$ is positive semidefinite with trace $1$ ; the weights need not sum to one, and the empty sum is allowed. Call it a separable state if it is also positive semidefinite with trace $1$ , and define

R_s(\rho)=\inf\{s\in\mathbb R:s\ge0,\ \exists\text{ separable state }\sigma,\ \rho+s\sigma\text{ is separable positive}\}.

This is a real infimum, with the total real-infimum convention giving $0$ for an empty set. Let $(\Omega_k)_{(i,j),(r,s)}=1/k$ when $i=j$ and $r=s$ , and $0$ otherwise, for indices less than $k$ . Then there exists a map $L$ from matrices on the $k\times k$ bipartite system to matrices on the $a\times b$ system that is a channel, maps every separable positive matrix to a separable positive matrix, and satisfies $L(\Omega_k)=\rho_\psi$ , if and only if $R_s(\rho_\psi)\le R_s(\Omega_k)$ . The channel requirement means a finite representation $L(X)=\sum_iK_iXK_i^\dagger$ with $\sum_iK_i^\dagger K_i=I$ ; the additional condition also explicitly requires a finite Kraus representation without a completeness requirement.

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