Theorem 10: negativity fails to be PPT-preserving monotone

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.negativity_notMonotone

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. There exist an integer $d>3$ , a density matrix $\rho$ on $d\times d$ , and a PPT-preserving channel $\Lambda$ on that register, for which

\mathcal N(\Lambda(\rho))>\mathcal N(\rho),\qquad \mathcal N(\rho)=\frac{\|\rho^\Gamma\|_1-1}{2}.

Here $\Gamma$ is first-party partial transpose. PPT-preserving means preserving the whole PPT positive cone.

This is an existential failure of 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)

/-- Theorem 10, PDF pp.13-14: existential failure of negativity monotonicity
under PPT preservation, rather than under the PPT-Choi condition. -/
theorem negativity_notMonotone :
    ∃ d : ℕ, 3 < d ∧ ∃ rho : Bip d d,
      ∃ L : Superop (Fin d × Fin d) (Fin d × Fin d),
        IsDensityMatrix rho ∧ IsChannel L ∧ PPTPreserving L ∧
        negativity rho < negativity (L rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 13, Theorem 10

Read-back

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

There exist a natural number $d>3$ , a positive semidefinite trace-one matrix $\rho$ on $\mathbb C^d\otimes\mathbb C^d$ , and a channel $L$ on that operator space such that $L$ preserves positive-partial-transpose matrices and $\mathcal N(\rho)<\mathcal N(L(\rho))$ . Here $L$ being a channel means $L(X)=\sum_jE_jXE_j^\dagger$ for a finite family with $\sum_jE_j^\dagger E_j=I$ ; its positive-partial-transpose preservation additionally requires a finite Kraus representation and asserts that, for every $X$ , if $X$ and $X^{T_A}$ are positive semidefinite, then $L(X)$ and $L(X)^{T_A}$ are positive semidefinite. The partial transpose is $(X^{T_A})_{(i,j),(i',j')}=X_{(i',j),(i,j')}$ , and $\mathcal N(X)=(\|X^{T_A}\|_1-1)/2$ , where $\|M\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{M^\dagger M}$ , with the square root taken by continuous functional calculus.

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