Theorem 11: superactivation of a non-entangling channel

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.nonEntangling_superactivation

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. There exists a channel $\Lambda$ on two qubits that is non-entangling, while

\Lambda\otimes\Lambda\text{ is not non-entangling across }AA^{\prime}:BB^{\prime}.

Thus this operation class is not closed under tensor products.

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 11, PDF pp.15-16: a two-qubit channel is non-entangling,
but its tensor square generates entanglement across AA':BB'. -/
theorem nonEntangling_superactivation :
    ∃ L : Superop (Fin 2 × Fin 2) (Fin 2 × Fin 2),
      IsChannel L ∧ NE L ∧ ¬ NE (tensorMaps L L) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

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

Read-back

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

There exists a channel $L$ on operators on $\mathbb C^2\otimes\mathbb C^2$ that is non-entangling, while its tensor square, with the two first-party factors grouped together and the two second-party factors grouped together, is not non-entangling. A channel has a finite representation $L(X)=\sum_jE_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=I$ ; being non-entangling means having a finite Kraus representation, without a normalization requirement, and preserving the cone of finite nonnegative sums of tensor products of positive semidefinite trace-one matrices, including the empty sum. Precisely, the grouped tensor-square map is defined by

\mathcal T(X)_{(c,g),(d,h);\,(c',g'),(d',h')} = \sum_{a,b,a',b',e,f,e',f'} X_{(a,e),(b,f);\,(a',e'),(b',f')} \,L(E_{(a,b),(a',b')})_{(c,d),(c',d')} \,L(E_{(e,f),(e',f')})_{(g,h),(g',h')},

where every scalar index ranges over $\{0,1\}$ and $E_{u,v}$ denotes a matrix unit; the conclusion is the negation of the entire non-entangling condition for $\mathcal T$ .

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