Theorem 20: strict hierarchy of k-non-entangling maps

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.kNonEntangling_strictHierarchy

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. For every $2\le k<d$ , there exists a completely positive map $\Lambda$ from $\mathbb C^d\otimes\mathbb C^d$ to two qubits such that

\Lambda\text{ is }k\text{-non-entangling},\qquad \Lambda\text{ is not }(k+1)\text{-non-entangling}.

Each nontrivial adjacent level of the hierarchy is distinct.

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 20, PDF pp.22-23: strictness of each k-non-entangling level,
for CP maps from d-by-d to two qubits; TP is not a hypothesis. -/
theorem kNonEntangling_strictHierarchy (k d : ℕ) (hk : 2 ≤ k) (hkd : k < d) :
    ∃ L : Superop (Fin d × Fin d) (Fin 2 × Fin 2),
      CP L ∧ KNE k L ∧ ¬ KNE (k + 1) L := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 22, Theorem 20

Read-back

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

For every pair of natural numbers $2\le k<d$ , there exists a map $L$ from matrices on $\mathbb C^d\otimes\mathbb C^d$ to matrices on $\mathbb C^2\otimes\mathbb C^2$ having a finite Kraus representation $L(X)=\sum_jK_jXK_j^\dagger$ , such that adjoining a $k$ -dimensional identity system to each party makes $L$ preserve separable positive operators, whereas adjoining a $(k+1)$ -dimensional identity system to each party does not. Explicitly, the amplified map acts on blocks by

\bigl[\widehat L_s(X)\bigr]_{(c,u),(e,v);\,(c',u'),(e',v')} = \left[ L\!\left( \bigl[X_{(a,u),(b,v);\,(a',u'),(b',v')}\bigr]_{(a,b),(a',b')} \right) \right]_{(c,e),(c',e')}.

It preserves the separable positive cone for $s=k$ , and there exists an operator in that cone whose image lies outside the corresponding cone for $s=k+1$ . A separable positive operator is a finite sum $\sum_jw_jA_j\otimes B_j$ with nonnegative weights and positive semidefinite trace- $1$ factors; empty sums are allowed and the weights need not sum to $1$ . No trace-preservation requirement is imposed on $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