Lemma 12: a channel from a bounded entanglement witness

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.witnessMap_duallyNonEntangling

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 $W$ be Hermitian and satisfy $\operatorname{Tr}(W\sigma)\ge0$ for every separable state, and let $\|W\|_F\le1$ be its Frobenius norm. Define $A=(W+2I)/3$ and

\Lambda(X)=\operatorname{Tr}(AX)\frac{I_4}{4}+\operatorname{Tr}((I-A)X)\phi_2^+.

Then $\Lambda$ is a channel and both $\Lambda$ and its trace dual preserve the separable positive cone.

This is the witness conversion construction used for distillability.

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 12, PDF pp.16-17: every witness of Frobenius norm at most one
constructs the specified dually non-entangling channel of Eq.(21). -/
theorem witnessMap_duallyNonEntangling {a b : ℕ} (ha : 0 < a) (hb : 0 < b)
    (W : Bip a b) (hw : Witness W) (hnorm : frobenius W ≤ 1) :
    IsChannel (witnessMap W) ∧ DNE (witnessMap W) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 16, Lemma 12

Read-back

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

For all positive natural numbers $a,b$ , let $W$ be a Hermitian matrix on $\mathbb C^a\otimes\mathbb C^b$ satisfying $\operatorname{Re}\operatorname{Tr}(WX)\ge0$ for every separable positive matrix $X$ , and suppose $\sqrt{\sum_{i,j}|W_{ij}|^2}\le1$ . Here separable positive matrices are finite nonnegative sums of tensor products of positive semidefinite trace-one matrices, including the empty sum. Put $A=(W+2I)/3$ and $\Phi_2=|\Omega_2\rangle\langle\Omega_2|$ , where $|\Omega_2\rangle=(|00\rangle+|11\rangle)/\sqrt2$ . Then the map $\Lambda_W(X)=\operatorname{Tr}(AX)I_4/4+\operatorname{Tr}((I-A)X)\Phi_2$ is a channel, and both $\Lambda_W$ and its trace-bilinear dual are non-entangling. Explicitly, the channel condition supplies a finite Kraus representation with $\sum_jE_j^\dagger E_j=I$ ; each non-entangling condition requires a finite Kraus representation, without a normalization requirement, and preservation of the separable positive cone. The dual is defined by $(\Lambda_W^\vee(Y))_{ij}=\operatorname{Tr}(\Lambda_W(E_{ji})Y)$ . Zero witnesses and one-dimensional input factors are included.

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