Exact and unbounded negativity ratio

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.negativity_unboundedRatio

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 integer $d>3$ , let $F_d$ be the swap, $\rho=(I-F_d)/(d(d-1))$ , $A=(dI+F_d)/(d+1)$ , and $\Lambda(X)=\operatorname{Tr}(AX)I_{d^2}/d^2+\operatorname{Tr}((I-A)X)\phi_d^+$ . Then $\rho$ is a state, $\Lambda$ is a PPT-preserving channel, and

\mathcal N(\rho)=\frac1d,\qquad\mathcal N(\Lambda(\rho))=\frac{d-1}{2d},\qquad\frac{\mathcal N(\Lambda(\rho))}{\mathcal N(\rho)}=\frac{d-1}{2}.

Consequently, for every real $C>0$ , some $d>3$ in this family has $0<\mathcal N(\rho)$ and $\mathcal N(\Lambda(\rho))>C\mathcal N(\rho)$ .

The dimension varies to produce arbitrary multiplicative increase.

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)

/-- PDF p.14: the exact ratio for the source's constructed state/channel,
and its consequence of an unbounded multiplicative increase as dimension varies. -/
theorem negativity_unboundedRatio :
    (∀ d : ℕ, 3 < d → IsDensityMatrix (antisymmetricDensity d) ∧
      IsChannel (negativityMap d) ∧ PPTPreserving (negativityMap d) ∧
      negativity (antisymmetricDensity d) = 1 / (d : ℝ) ∧
      negativity (negativityMap d (antisymmetricDensity d)) = ((d : ℝ) - 1) / (2 * d) ∧
      negativity (negativityMap d (antisymmetricDensity d)) / negativity (antisymmetricDensity d) =
        ((d : ℝ) - 1) / 2) ∧
    (∀ C : ℝ, 0 < C → ∃ d : ℕ, 3 < d ∧
      0 < negativity (antisymmetricDensity d) ∧
      C * negativity (antisymmetricDensity d) < negativity (negativityMap d (antisymmetricDensity d))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 14, unbounded-negativity-ratio

Read-back

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

For each natural number $d>3$ , define

F_d|i,j\rangle=|j,i\rangle,\qquad A_d=\frac{I_{d^2}-F_d}{d(d-1)},\qquad \Phi_d=\frac1d\sum_{i,j=0}^{d-1}|i,i\rangle\langle j,j|, \qquad B_d=\frac{dI_{d^2}+F_d}{d+1},

and

L_d(X)=\operatorname{Tr}(B_dX)\frac{I_{d^2}}{d^2} +\operatorname{Tr}((I_{d^2}-B_d)X)\Phi_d.

Then $A_d$ is positive semidefinite with trace $1$ , and $L_d$ is a channel: it admits a finite Kraus representation with $\sum_jK_j^\dagger K_j=I$ . It also preserves operators that are both positive semidefinite and positive semidefinite after partial transpose on the first party; this preservation predicate additionally requires a finite Kraus representation. Define

\mathcal N(X)=\frac{\|X^{\Gamma_A}\|_1-1}{2}, \qquad (X^{\Gamma_A})_{(i,j),(i',j')}=X_{(i',j),(i,j')}, \qquad \|Y\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{Y^\dagger Y}.

The asserted values are

\mathcal N(A_d)=\frac1d,\qquad \mathcal N(L_d(A_d))=\frac{d-1}{2d},\qquad \frac{\mathcal N(L_d(A_d))}{\mathcal N(A_d)}=\frac{d-1}{2}.

Furthermore, for every real $C>0$ , there exists a natural number $d>3$ such that $\mathcal N(A_d)>0$ and $C\,\mathcal N(A_d)<\mathcal N(L_d(A_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