Theorem 9: arbitrary Schmidt ranks under dually non-entangling channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.duallyNonEntangling_ranks

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 pair of integers $k,d\ge2$ , there exist pure states $\psi$ on $k\times k$ and $\varphi$ on $d\times d$ , and a dually non-entangling channel $\Lambda$ , such that

\operatorname{SR}(\psi)=k,\quad\operatorname{SR}(\varphi)=d,\quad\Lambda(\psi)=\varphi.

The two ranks need not be ordered.

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 9, PDF pp.12-13: arbitrary two positive Schmidt ranks at least two
can be connected by a dually non-entangling channel, with no k<d restriction. -/
theorem duallyNonEntangling_ranks (k d : ℕ) (hk : 2 ≤ k) (hd : 2 ≤ d) :
    ∃ psi : UnitBipartiteKet k k, ∃ phi : UnitBipartiteKet d d,
      ∃ L : Superop (Fin k × Fin k) (Fin d × Fin d),
        finiteSchmidtRank psi.ket = k ∧ finiteSchmidtRank phi.ket = d ∧
        IsChannel L ∧ DNE L ∧ L psi.rho = phi.rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 12, Theorem 9

Read-back

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

For every pair of natural numbers $k,d\ge2$ , there exist unit vectors $\psi\in\mathbb C^k\otimes\mathbb C^k$ and $\phi\in\mathbb C^d\otimes\mathbb C^d$ , and a channel $L$ between their operator spaces, such that the first marginal of $|\psi\rangle\langle\psi|$ has exactly $k$ strictly positive eigenvalues, the first marginal of $|\phi\rangle\langle\phi|$ has exactly $d$ strictly positive eigenvalues, and $L(|\psi\rangle\langle\psi|)=|\phi\rangle\langle\phi|$ . For a vector $v$ , this marginal has entries $\sum_jv_{ij}\overline{v_{i'j}}$ . Both $L$ and its trace-bilinear dual $L^\vee$ , defined by $(L^\vee(Y))_{ij}=\operatorname{Tr}(L(E_{ji})Y)$ , must have finite Kraus representations and map every separable positive matrix to a separable positive matrix. Such a matrix is a finite nonnegative sum of tensor products of positive semidefinite trace-one matrices, with the empty sum allowed. The channel requirement additionally gives a representation $L(X)=\sum_jE_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=I$ . There is no required ordering between $k$ and $d$ .

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