Corollary 2: non-entangling channels can increase Schmidt rank

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.schmidtRank_increase

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. For integers $2\le k<d$ , there exist a pure state $\varphi$ on $\mathbb C^d\otimes\mathbb C^d$ and a non-entangling channel $\Lambda$ from $k\times k$ to $d\times d$ such that

\Lambda(\phi_k^+)=\varphi,\qquad \operatorname{SR}(\varphi)=d.

Schmidt rank counts the positive squared Schmidt coefficients. This witnesses failure of Schmidt-rank monotonicity.

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)

/-- Corollary 2, PDF p.9: currency of rank k can produce a pure state of rank d>k. -/
theorem schmidtRank_increase (k d : ℕ) (hk : 2 ≤ k) (hkd : k < d) :
    ∃ phi : UnitBipartiteKet d d, ∃ L : Superop (Fin k × Fin k) (Fin d × Fin d),
      IsChannel L ∧ NE L ∧ L (epr k) = phi.rho ∧ finiteSchmidtRank phi.ket = d := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 9, Corollary 2

Read-back

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

For every pair of natural numbers $k,d$ satisfying $2\le k<d$ , there exist a complex Euclidean vector $\phi$ on $\{0,\ldots,d-1\}^2$ with $\|\phi\|=1$ , and a map $L$ from matrices on $\{0,\ldots,k-1\}^2$ to matrices on $\{0,\ldots,d-1\}^2$ , such that $L$ is a channel, has a finite Kraus representation, preserves separable positive matrices, and

L(\Omega_k)=\phi\phi^\dagger,\qquad \#\{i<d:\lambda_i>0\}=d.

Here a channel has a finite Kraus representation $L(X)=\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ ; a separable positive matrix is a finite sum $\sum_jw_jA_j\otimes B_j$ with nonnegative weights and positive semidefinite trace-one factors, without requiring the weights to sum to one; $\Omega_k$ has entry $1/k$ at $((i,i),(r,r))$ and zero at all other entries; and $\lambda_0,\ldots,\lambda_{d-1}$ are the eigenvalues, in descending order and with multiplicity, of the reduced matrix

(\rho_A)_{i,r}=\sum_{j<d}\phi(i,j)\overline{\phi(r,j)}.

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