Lemma 1, Eqs.(8)–(10): PBT diamond error

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.pbt_diamond_error

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

prove2quantum

Let $d\ge2$ and let $\Gamma_{d,M}$ be the deterministic PBT channel using integer $M\ge2$ , $M$ normalized Bell pairs, the standard square-root measurement, classical communication of its outcome, and port selection. Let $f_e=\langle\Phi_d|(\mathrm{id}\otimes\Gamma_{d,M})(\Phi_d)|\Phi_d\rangle$ , with normalized $|\Phi_d\rangle=d^{-1/2}\sum_j|j,j\rangle$ . The channel is CPTP and depolarizing: $\Gamma(X)=(1-\xi_{d,M})X+\xi_{d,M}\operatorname{tr}(X)I/d$ . Its actual unhalved diamond error satisfies

\delta_{d,M}=2(1-f_e)=\frac{2(d^2-1)}{d^2}\xi_{d,M}\le\frac{2d(d-1)}M.

Moreover $\delta_{d,M}\to0$ as integer $M\to\infty$ . These identities relate the operational PBT construction to its depolarizing probability and give uniform convergence, including reference-entangled inputs.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P49

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P49

open QAlgorithms Filter

open scoped Matrix ComplexConjugate ComplexOrder BigOperators

attribute [local instance] Classical.propDecidable Classical.decEq

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

open QAlgorithms.Papers.Independent.Dependency50.P18 (bipartiteTensor)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond AdaptiveTest adaptiveInput adaptiveAccept)

open QAlgorithms.Papers.Independent.Bridge50.P25
  (LOCCOn normalizedChannelChoi TwoWayGenerationCode TwoWayChannelProtocol
   generationCodeError twoWayGenerationCapacity sendChannelRegister StateFunctional
   IsDimensionChangingLOCCMonotone privateStateInPartyOrder)

open QAlgorithms.Papers.Independent.Support50.P07 (amplitudeDampingChannel)

/-- Lemma 1, PDF p.3, (8)--(10), Methods pp.7--8: actual SRM PBT is
CPTP and depolarizing; full diamond error equals twice Bell infidelity.
The error bound is uniform over all inputs, including entangled references. -/
theorem pbt_diamond_error (d : ℕ) [NeZero d] (hd : 2 ≤ d) :
    (∀ M : ℕ, 2 ≤ M →
      IsChannel (pbtChannel d M) ∧
      (∀ X, pbtChannel d M X = ((1-pbtNumber d M : ℝ) : ℂ) • X +
        ((pbtNumber d M / d : ℝ) : ℂ) • (X.trace • (1 : Mat (Fin d)))) ∧
      pbtError d M = 2 * (1-pbtEntanglementFidelity d M) ∧
      pbtError d M = 2 * ((d : ℝ)^2-1) / (d : ℝ)^2 * pbtNumber d M ∧
      pbtError d M ≤ 2 * (d : ℝ) * (d-1 : ℝ) / M) ∧
    Tendsto (pbtError d) atTop (nhds 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 3, Lemma 1, Eqs.(8)–(10): PBT diamond error

Read-back

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

For every natural number $d$ , equipped with the assumption $d\ne0$ , and satisfying $d\ge2$ , the following holds. To specify the quantities involved, write $\mathcal P_{d,M}$ for the map constructed as follows: on an input register and $M$ ports, each of dimension $d$ , define

S_i[(x,a),(y,b)] =\begin{cases} 1/d,&x=a_i,\ y=b_i,\ \text{and }a_j=b_j\text{ for every }j\ne i,\\ 0,&\text{otherwise}, \end{cases} \quad S=\sum_{i=0}^{M-1}S_i,\quad R=f(S),\quad f(t)=(\sqrt t)^{-1},

where $f(S)$ uses continuous functional calculus and $f(0)=0$ , and put

Q_i=RS_iR+\frac1M(I-RSR).

For ports of output dimension $e$ , define the selection map by

\mathcal T_{d,e,M}(Z)_{u,v} =\sum_{\substack{i,\ p,q,\ b,c\\ b_i=u,\ c_i=v\\ b_j=c_j\ (j\ne i)}} (Q_i)_{q,p}\,Z_{(p,b),(q,c)},

where $p,q$ index the input register together with its $d$ -dimensional ports, and $b,c$ index the $e$ -dimensional ports; the singleton output register is suppressed. With $\Phi_d=d^{-1}\sum_{x,y}|x,x\rangle\langle y,y|$ , set $\mathcal P_{d,M}(X)=\mathcal T_{d,d,M}(X\otimes\Phi_d^{\otimes M})$ . For any matrix $X$ , let $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , and for a map $\mathcal F$ with input dimension $d$ , let

\Delta_d(\mathcal F) =\sup_{\|X\|_1\le1}\|(\operatorname{id}_d\otimes\mathcal F)(X)\|_1,

where $X$ ranges over all complex matrices on the two $d$ -dimensional registers. Define

\nu_{d,M}=1-\operatorname{Re}\bigl(\mathcal P_{d,M}(|0\rangle\langle1|)_{0,1}\bigr),\quad \varepsilon_{d,M}=\Delta_d(\operatorname{id}-\mathcal P_{d,M}),

and

F_{d,M} =\operatorname{Re}\langle\Omega_d| (\operatorname{id}_d\otimes\mathcal P_{d,M})(\Phi_d) |\Omega_d\rangle,\qquad |\Omega_d\rangle=d^{-1/2}\sum_x|x,x\rangle.

For every natural number $M\ge2$ , $\mathcal P_{d,M}$ has a finite Kraus representation $X\mapsto\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ , and, for every complex $d\times d$ matrix $X$ ,

\mathcal P_{d,M}(X) =(1-\nu_{d,M})X+\frac{\nu_{d,M}}d\,\operatorname{tr}(X)I.

Moreover,

\varepsilon_{d,M} =2(1-F_{d,M}) =\frac{2(d^2-1)}{d^2}\nu_{d,M} \le\frac{2d(d-1)}M, \qquad \lim_{M\to\infty}\varepsilon_{d,M}=0.

The finite- $M$ assertions require $M\ge2$ ; the convergence assertion concerns the entire naturally indexed sequence.

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