Standard robustness is non-entangling monotone

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.robustness_monotone

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 every bipartite state $\rho$ and non-entangling channel $\Lambda$ between arbitrary positive local dimensions,

R(\Lambda(\rho))\le R(\rho).

Here $R$ is standard robustness, using separable normalized noise.

This extends the robustness comparison to arbitrary mixed states.

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.8, paragraph preceding Theorem 1: standard robustness monotonicity
under non-entangling channels on arbitrary mixed states. -/
theorem robustness_monotone {a b c d : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d)
    (rho : Bip a b) (hrho : IsDensityMatrix rho)
    (L : Superop (Fin a × Fin b) (Fin c × Fin d)) (hL : IsChannel L) (hne : NE L) :
    standardStateRobustness (L rho) ≤ standardStateRobustness rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 8, robustness-monotonicity

Read-back

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

For positive natural numbers $a,b,c,d$ , let $\rho$ be a positive semidefinite trace- $1$ matrix on $\mathbb C^a\otimes\mathbb C^b$ , and let $L$ map matrices on this space to matrices on $\mathbb C^c\otimes\mathbb C^d$ . Assume that $L(X)=\sum_jK_jXK_j^\dagger$ for a finite family with $\sum_jK_j^\dagger K_j=I$ , and that $L$ preserves separable positive operators; these are the channel and $NE$ assumptions, with $NE$ also requiring a finite Kraus representation. For either bipartite space, let $\mathcal S_+$ consist of all finite sums $\sum_jw_jA_j\otimes B_j$ with $w_j\ge0$ and positive semidefinite trace- $1$ factors, allowing the empty sum and imposing no normalization on the weights, and define

R(\tau)= \inf\left\{ s\in\mathbb R: s\ge0,\ \exists\sigma\in\mathcal S_+,\ \sigma\ge0,\ \operatorname{Tr}\sigma=1,\ \tau+s\sigma\in\mathcal S_+ \right\}.

Then $R(L(\rho))\le R(\rho)$ . This is the real infimum appearing in the definition of standard state robustness.

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