Proposition 1 / SDP (6): NS and NS∩PPT minimum simulation error

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.minimumError_sdp

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

All systems have finite positive dimension and fixed computational bases. Matrix order is Loewner order and logarithms are base two.

Let $\mathcal N:A_o\to B_i$ and $\mathcal M:A_i\to B_o$ be CPTP maps. Let $\omega_\Omega(\mathcal N,\mathcal M)$ be the infimum half-diamond simulation error over codes with assistance $\Omega$ . For a Hermitian matrix $Z$ on $(A_iB_i)(A_oB_o)$ define $J_{\rm eff}=\operatorname{Tr}_{A_oB_i}[(J_{\mathcal N}^{T}\otimes I_{A_iB_o})Z]$ , with registers reordered as indicated. Then

\omega_{\rm NS}(\mathcal N,\mathcal M)=\inf\{\gamma:\operatorname{Tr}_{B_o}Y\le\gamma I_{A_i},\ Y\ge J_{\rm eff}-J_{\mathcal M},\ Y\ge0,\ Z\text{ satisfies (6e)--(6g)}\}.

The explicitly encoded constraints (6e)--(6g) are $Z\ge0$ , $\operatorname{Tr}_{A_oB_o}Z=I_{A_iB_i}$ , $\operatorname{Tr}_{A_o}Z=(I_{A_i}/|A_i|)\otimes\operatorname{Tr}_{A_oA_i}Z$ , and $\operatorname{Tr}_{B_o}Z=(I_{B_i}/|B_i|)\otimes\operatorname{Tr}_{B_iB_o}Z$ . The infimum ranges over all $\gamma,Y,Z$ . Adding $Z^{T_{B_iB_o}}\ge0$ gives exactly $\omega_{\rm NS\cap PPT}$ . This characterizes noisy-resource simulation by matrix optimization.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P65

Formal statement

noncomputable section

open Filter QAlgorithms

open scoped BigOperators Matrix ComplexConjugate ComplexOrder Topology

namespace QAlgorithms.Papers.Independent.Intakethird100.P65

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P09 (transposeBob)

open QAlgorithms.Papers.Independent.Dependency50.P35 (maxRelative)

open QAlgorithms.Papers.Independent.Independent2.P01 (dampingKraus damping)

open QAlgorithms.Papers.Independent.Gap48.P33 (phaseFlipChannel)

open QAlgorithms.Papers.Independent.Information100.P06 (Below)

open QAlgorithms.Papers.Independent.Information100.P34 (choi)

open QAlgorithms.Papers.Independent.Information100.P62 (Stochastic)

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P67 (IsSubnormalized purifiedDistance)

open QAlgorithms.Papers.Independent.Information100.P69 (replacer permute)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond channelPower channelRelative)

open QAlgorithms.Papers.Independent.Support50.P39 (quantumMutualInformation)

variable {A B C D R : Type} [Fintype A] [DecidableEq A]
  [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C]
  [Fintype D] [DecidableEq D] [Fintype R] [DecidableEq R]

variable [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] [Nonempty R]

/-- Proposition 1, SDP (6), PDF p.4. Both NS and NS-intersect-PPT conclusions. -/
theorem minimumError_sdp (N : Superop B C) (M : Superop A D)
    (hN : IsChannel N) (hM : IsChannel M) :
    minimumError .ns N M = sInf {g : ℝ | generalErrorFeasible false N M g} ∧
    minimumError .nsPpt N M = sInf {g : ℝ | generalErrorFeasible true N M g} := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P65

end

Source

Quantum Channel Simulation and the Channel's Smooth Max-Information, arXiv:1807.05354v2, PDF p. 4, Proposition 1 / SDP (6): NS and NS∩PPT minimum simulation error

Read-back

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

For finite index types $A,B,C,D$ , with decidable equality, let $N$ map complex matrices on $B$ to matrices on $C$ , and let $M$ map matrices on $A$ to matrices on $D$ . Assume both maps admit finite Kraus representations $X\mapsto\sum_iK_iXK_i^\dagger$ with $\sum_iK_i^\dagger K_i=I$ . Write $J_F((a,b),(a',b'))=F(|a\rangle\langle a'|)_{b,b'}$ , $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , and $\|\Delta\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes\Delta)(X)\|_1$ , where $X$ ranges over all complex matrices on $A\times A$ , without a positivity requirement. A permitted nonsignalling map $P:A\times C\to B\times D$ is a channel for which there are channels $F:A\to B$ and $G:C\to D$ satisfying $\operatorname{Tr}_D P(X)=F(\operatorname{Tr}_C X)$ and $\operatorname{Tr}_B P(X)=G(\operatorname{Tr}_A X)$ for every matrix $X$ . In the PPT variant, additionally require that partially transposing the $C$ input, applying $P$ , and partially transposing the $D$ output gives a channel. Define

\mathcal W_N(P)(X)_{b,d} =\sum_{a,c\in B}\sum_{u,v\in C} N(|a\rangle\langle c|)_{u,v}\, P(X\otimes|u\rangle\langle v|)_{(a,b),(c,d)}.

For each variant, the infimum of $\tfrac12\|\mathcal W_N(P)-M\|_\diamond$ over its permitted maps equals the infimum of all real $g$ for which there exist Hermitian-indexed matrices $Y$ on $A\times D$ and $Z$ on $(A\times C)\times(B\times D)$ satisfying $Y\ge0$ , $gI_A-\operatorname{Tr}_D Y\ge0$ , and

Y-\bigl(\mathcal L(J_N,Z)-J_M\bigr)\ge0,\qquad \mathcal L(J_N,Z)_{(i,b),(j,d)} =\sum_{a,c\in B}\sum_{u,v\in C} (J_N)_{(a,u),(c,v)} Z_{((i,u),(a,b)),((j,v),(c,d))}.

Here the constraints on $Z$ are $Z\ge0$ and, for every choice of the displayed indices,

\begin{aligned} \sum_{a,b}Z_{((i,u),(a,b)),((j,v),(a,b))} &=\delta_{ij}\delta_{uv},\\ \sum_aZ_{((i,u),(a,b)),((j,v),(a,d))} &=\frac{\delta_{ij}}{|A|} \sum_{k,a}Z_{((k,u),(a,b)),((k,v),(a,d))},\\ \sum_bZ_{((i,u),(a,b)),((j,v),(c,b))} &=\frac{\delta_{uv}}{|C|} \sum_{w,b}Z_{((i,w),(a,b)),((j,w),(c,b))}. \end{aligned}

The PPT variant also requires positivity of the matrix whose $(x,y)$ entry is $Z_{((x_A,y_C),(x_B,y_D)),((y_A,x_C),(y_B,x_D))}$ . Partial traces mean summing matching indices of the discarded factor. Neither equality asserts attainment of its infimum; $g$ has no separately stated sign restriction, and all divisions use total field division, including $1/0=0$ .

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