Theorem 3, Eq.(20): universal adaptive channel-discrimination lower bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.adaptive_discrimination_lower_bound

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

prove2quantum

Let $\mathcal E_0,\mathcal E_1:\mathbb C^d\to\mathbb C^e$ be CPTP channels, with $d\ge2$ and $e\ge1$ . Their equally likely labels are unknown to the adaptive protocol. Let $p_n$ be the infimum of the error over normalized preparations, arbitrary finite memories, label-independent CPTP interleavings, exactly $n$ channel calls, and final binary POVMs. Write $\rho_u$ for the normalized, reference-first Choi state and $D(\rho,\sigma)=\|\rho-\sigma\|_1/2$ . For integer $M\ge2$ , let $\delta_{d,M}$ be the unhalved diamond error of standard deterministic $M$ -port PBT and define

B_M=\frac{1-n\delta_{d,M}-D(\rho_0^{\otimes nM},\rho_1^{\otimes nM})}{2}.

For every $n\ge1$ , $p_n\ge B_M$ for every such $M$ , and hence $p_n\ge\sup_{M\ge2}B_M$ . Also $p_0=1/2$ . No distinctness premise or finite optimizer is required. This is an operational bound uniform over all adaptive discrimination strategies.

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)

/-- Theorem 3, PDF p.4, (20): every integer M gives a universal lower bound;
no finite maximizer is asserted. The no-probing case has error exactly 1/2. -/
theorem adaptive_discrimination_lower_bound (d e : ℕ) [NeZero d] [NeZero e]
    (hd : 2 ≤ d) (E0 E1 : Superop (Fin d) (Fin e))
    (h0 : IsChannel E0) (h1 : IsChannel E1) :
    symmetricAdaptiveError 0 E0 E1 = 1/2 ∧
    (∀ n : ℕ, 1 ≤ n → ∀ M : ℕ, 2 ≤ M →
      universalBound n M E0 E1 ≤ symmetricAdaptiveError n E0 E1) ∧
    (∀ n : ℕ, 1 ≤ n →
      (⨆ M : {m : ℕ // 2 ≤ m}, universalBound n M.val E0 E1) ≤ symmetricAdaptiveError n E0 E1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 4, Theorem 3, Eq.(20): universal adaptive channel-discrimination lower bound

Read-back

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

For natural numbers $d,e$ with $d\ne0$ , $e\ne0$ , and $2\le d$ , and channels $\mathcal E_0,\mathcal E_1$ from complex $d\times d$ matrices to complex $e\times e$ matrices, the assertion is

\beta_0=\frac12,\qquad \forall n\ge1\ \forall M\ge2,\quad B_{n,M}\le\beta_n,\qquad \forall n\ge1,\quad \sup_{M\ge2}B_{n,M}\le\beta_n,

where all indices $n,M$ are natural numbers. Each channel assumption means a finite Kraus representation $\mathcal E_i(X)=\sum_jK_{i,j}XK_{i,j}^\dagger$ with $\sum_jK_{i,j}^\dagger K_{i,j}=I$ . Define $\beta_0=1/2$ ; for $n>0$ , define $\beta_n$ as the real infimum of $(1-a_P(\mathcal E_0)+a_P(\mathcal E_1))/2$ over all tests $P$ consisting of a positive memory dimension $r$ , a positive semidefinite initial matrix $\rho_0$ of trace $1$ on $\mathbb C^r\otimes\mathbb C^d$ , a finite-Kraus channel $\mathcal B_k$ from the memory–output space to the memory–input space for every $k\in\mathbb N$ , and an effect $0\le T\le I$ on the memory–output space. With blockwise extension $\widehat{\mathcal E}(X)_{(u,b),(v,c)}=\mathcal E((X_{(u,i),(v,j)})_{i,j})_{b,c}$ , set $\rho_{k+1}^{\mathcal E}=\mathcal B_k(\widehat{\mathcal E}(\rho_k^{\mathcal E}))$ and $a_P(\mathcal E)=\operatorname{Re}\operatorname{Tr}(T\widehat{\mathcal E}(\rho_{n-1}^{\mathcal E}))$ . The lower-bound scalar is

B_{n,M}= \frac{1-n\|\mathrm{id}-\mathcal P_{d,M}\|_\diamond -\tfrac12\|C_0^{[nM]}-C_1^{[nM]}\|_1}{2}.

Here $C_i((a,b),(a',b'))=\mathcal E_i(d^{-1}|a\rangle\langle a'|)_{b,b'}$ , $C^{[s]}(x,y)=\prod_{j<s}C(x_j,y_j)$ , $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , and $\|F\|_\diamond=\sup_{\|X\|_1\le1}\|\widehat F(X)\|_1$ , using a $d$ -dimensional reference and the same blockwise extension rule. To specify $\mathcal P_{d,M}$ , let $S_i((a,u),(b,v))=d^{-1}$ if $a=u_i$ , $b=v_i$ , and $u_j=v_j$ for all $j\ne i$ , and $0$ otherwise, for $i<M$ and $u,v\in[d]^M$ . Set $S=\sum_iS_i$ , $R=f(S)$ by continuous functional calculus with $f(x)=(\sqrt x)^{-1}$ , and $Q_i=RS_iR+M^{-1}(I-RSR)$ . Then

\mathcal P_{d,M}(X)_{b,c} =d^{-M}\sum_{i<M}\sum_{a,a'<d} \sum_{\substack{u,v\in[d]^M\\u_i=b,\ v_i=c\\u_j=v_j\ (j\ne i)}} Q_i((a',v),(a,u))X_{a,a'}.

The inverse at a zero eigenvalue is $0$ . The theorem’s bounds apply to every positive $n$ and every $M\ge2$ , including $n=1$ ; its separate zero-use assertion is exactly $\beta_0=1/2$ .

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