Lemma 18: compressed Choi criterion for k-non-entangling maps

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.kNonEntangling_compression

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. Let $1\le k\le d$ and let $\Lambda$ be a CP endomap on $d\times d$ . A $k$ -dimensional projection means a rectangular coisometry $P:\mathbb C^d\to\mathbb C^k$ , with $PP^\dagger=I_k$ . Then

\Lambda\text{ is }k\text{-non-entangling}\ \Longleftrightarrow\ (I_{d^2}\otimes P\otimes Q)J(\Lambda)(I_{d^2}\otimes P\otimes Q)^\dagger\text{ is separable for every such }P,Q.

The output partition groups $A_{\rm out}\mathbb C^k:B_{\rm out}\mathbb C^k$ .

This tests the whole amplified separable cone using coisometries.

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)

/-- Lemma 18, PDF p.21: coisometry compression criterion on the stated
endomap, with the dimensional domain 1<=k<=d made explicit. -/
theorem kNonEntangling_compression {d k : ℕ} (hk : 1 ≤ k) (hkd : k ≤ d)
    (L : Superop (Fin d × Fin d) (Fin d × Fin d)) (hcp : CP L) :
    KNE k L ↔ ∀ P Q : Matrix (Fin k) (Fin d) ℂ,
      Coisometry P → Coisometry Q → IsSeparablePositive (compressChoi L P Q) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 21, Lemma 18

Read-back

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

For natural numbers $1\le k\le d$ , let $L$ map complex matrices on $\mathbb C^d\otimes\mathbb C^d$ to matrices on the same space, and assume that $L(X)=\sum_{j=1}^m K_jXK_j^\dagger$ for some finite family of matrices $K_j$ , with no normalization condition imposed on this family. Call an operator separable positive if it is a finite sum $\sum_j w_j A_j\otimes B_j$ , where $w_j\ge0$ and each $A_j,B_j$ is positive semidefinite with trace $1$ ; the empty sum is allowed, and the weights need not sum to $1$ . Then adjoining a $k$ -dimensional identity system to each party makes $L$ preserve separable positive operators if and only if, for every $P,Q\in\mathbb C^{k\times d}$ satisfying $PP^\dagger=QQ^\dagger=I_k$ , the operator

\bigl((I_d\otimes P)\otimes(I_d\otimes Q)\bigr)\, C_L\, \bigl((I_d\otimes P)\otimes(I_d\otimes Q)\bigr)^\dagger

is separable positive across $(\mathbb C^d\otimes\mathbb C^k):(\mathbb C^d\otimes\mathbb C^k)$ . Here the party-grouped Choi operator is defined by

(C_L)_{(c,a),(e,b);\,(c',a'),(e',b')} = \bigl[L(|a,b\rangle\langle a',b'|)\bigr]_{(c,e),(c',e')},

and adjoining the identity systems means applying $L$ to every matrix block obtained by fixing the two ancillary row indices and two ancillary column indices. This preservation condition, together with $k>0$ and the finite Kraus representation of $L$ , is precisely the predicate $KNE(k,L)$ .

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