Corollary 2 / SDP (9): noiseless-resource reduced minimum error

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.noiselessError_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\to B$ be CPTP and let $m\ge1$ be an integer. Put $\omega_\Omega(\mathrm{id}_m,\mathcal N)$ for the minimum half-diamond error using one noiseless $m$ -dimensional resource. Then

\omega_{\rm NS}(\mathrm{id}_m,\mathcal N)=\inf\gamma

subject to $Y\ge J- J_{\mathcal N}$ , $Y\ge0$ , $\operatorname{Tr}_B Y\le\gamma I_A$ , $J\ge0$ , $\operatorname{Tr}_B J=I_A$ , $J\le I_A\otimes V_B$ , and $\operatorname{Tr}V_B=m^2$ . All $Y,J,V_B$ are bound Hermitian optimization variables. For NS-intersect-PPT assistance add $-I_A\otimes V_B^T\le mJ^{T_B}\le I_A\otimes V_B^T$ . This reduction includes $m=1$ , where feasible effective channels are constant.

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]

/-- Corollary 2, SDP (9), PDF pp.5--6. Resource dimension m=1 is included. -/
theorem noiselessError_sdp (N : Superop A B) (hN : IsChannel N) (m : ℕ) (hm : 0 < m) :
    minimumError .ns (fun X : Mat (Fin m) => X) N =
      sInf {g : ℝ | reducedErrorFeasible false N m g} ∧
    minimumError .nsPpt (fun X : Mat (Fin m) => X) N =
      sInf {g : ℝ | reducedErrorFeasible 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. 5, Corollary 2 / SDP (9): noiseless-resource reduced minimum error

Read-back

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

For finite index types $A,B$ , with decidable equality, let $N$ be a channel from matrices on $A$ to matrices on $B$ , meaning $N(X)=\sum_iK_iXK_i^\dagger$ for a finite family with $\sum_iK_i^\dagger K_i=I_A$ , and let $m$ be any positive natural number, including $m=1$ . The minimum simulation error using the identity channel on $\mathbb C^m$ , both with nonsignalling assistance and with nonsignalling PPT assistance, equals the corresponding infimum described below. A nonsignalling assistance map $P:A\times\{0,\ldots,m-1\}\to\{0,\ldots,m-1\}\times B$ is a channel whose two output marginals depend only on their respective input marginals, through channels, for every input matrix; PPT assistance additionally requires that partial transpose on its second input and second output makes $P$ a channel. Its induced map is

\mathcal W(P)(X)_{b,b'} =\sum_{u,v=0}^{m-1} P(X\otimes|u\rangle\langle v|)_{(u,b),(v,b')}.

The minimum error is the infimum over permitted $P$ of $\tfrac12\|\mathcal W(P)-N\|_\diamond$ , where $\|\Delta\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes\Delta)(X)\|_1$ , $X$ ranges over all matrices on $A\times A$ , and $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . For nonsignalling assistance this equals the infimum of real $g$ for which there are matrices $Y,J$ on $A\times B$ and a Hermitian matrix $V$ on $B$ such that

Y\ge0,\quad gI_A-\operatorname{Tr}_B Y\ge0,\quad Y-J+J_N\ge0,\quad J\ge0,\quad \operatorname{Tr}_B J=I_A,\quad I_A\otimes V-J\ge0,\quad \operatorname{Re}\operatorname{tr}V=m^2,

with $J_N((a,b),(a',b'))=N(|a\rangle\langle a'|)_{b,b'}$ . For nonsignalling PPT assistance, the infimum has the same constraints and additionally

-I_A\otimes V^{\mathsf T}\ \le\ mJ^{\Gamma_B}\ \le\ I_A\otimes V^{\mathsf T}, \qquad (J^{\Gamma_B})_{(a,b),(a',b')}=J_{(a,b'),(a',b)}.

Each matrix inequality means that the right side minus the left side is positive semidefinite, and each partial trace sums matching discarded indices. No attainment is asserted.

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