§II.J, Eqs.(34),(37): adaptive lower and block bounds

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.amplitude_damping_discrimination

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

prove2quantum

Let $p,q\in[0,1]$ , $n\ge1$ , and integer $M\ge2$ . Write $F=[1+\sqrt{(1-p)(1-q)}+\sqrt{pq}]/2$ , $\Delta_M(p)=\xi_M[(1-p)/2+\sqrt{1-p}]$ , and $\overline\Delta_M=[\Delta_M(p)+\Delta_M(q)]/2$ . The equally likely amplitude-damping channels satisfy

p_n\ge\frac{1-n\overline\Delta_M-\sqrt{1-F^{2nM}}}{2}.

For independent Bell probes with one joint optimal measurement, let $p_n^{\rm block}=[1-D(\rho_{\mathcal E_p}^{\otimes n},\rho_{\mathcal E_q}^{\otimes n})]/2$ . Then

p_n\le p_n^{\rm block},\qquad\frac{1-\sqrt{1-F^{2n}}}{2}\le p_n^{\rm block}\le\frac{F^n}{2}.

The block lower bound constrains the block strategy alone; the exact adaptive optimum remains unspecified.

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)

/-- PDF pp.6--7, (34),(37): adaptive lower bound and distinct nonadaptive
block sandwich. No claim of optimality of the block strategy is made. -/
theorem amplitude_damping_discrimination (n M : ℕ) (hn : 1 ≤ n) (hM : 2 ≤ M)
    (p q : ℝ) (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) :
    let E0 := amplitudeDampingChannel p
    let E1 := amplitudeDampingChannel q
    let F := dampingFidelity p q
    (1-n*((dampingSimulationError M p+dampingSimulationError M q)/2) -
      Real.sqrt (1-F^(2*n*M)))/2 ≤ symmetricAdaptiveError n E0 E1 ∧
    symmetricAdaptiveError n E0 E1 ≤ bellProbeBlockError n E0 E1 ∧
    (1-Real.sqrt (1-F^(2*n)))/2 ≤ bellProbeBlockError n E0 E1 ∧
    bellProbeBlockError n E0 E1 ≤ F^n/2 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 6, §II.J, Eqs.(34),(37): adaptive lower and block bounds

Read-back

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

For every pair of natural numbers $n\ge1$ , $M\ge2$ , and real numbers $p,q\in[0,1]$ , let $\mathcal E_0=\mathcal A_p$ and $\mathcal E_1=\mathcal A_q$ , where

\mathcal A_r(X)=K_{r,0}XK_{r,0}^\dagger+K_{r,1}XK_{r,1}^\dagger,\quad K_{r,0}=\begin{pmatrix}1&0\\0&\sqrt{1-r}\end{pmatrix},\quad K_{r,1}=\begin{pmatrix}0&\sqrt r\\0&0\end{pmatrix}.

Set

F=\frac{1+\sqrt{(1-p)(1-q)}+\sqrt{pq}}2.

To define the simulation terms, construct $\mathcal P_M$ from the qubit signals $S_i[(x,a),(y,b)]=\frac12\mathbf1_{\{x=a_i,\ y=b_i,\ a_j=b_j\ \forall j\ne i\}}$ , $S=\sum_iS_i$ , $R=f(S)$ with $f(t)=(\sqrt t)^{-1}$ , $f(0)=0$ , and $Q_i=RS_iR+M^{-1}(I-RSR)$ : on $X\otimes\Phi_2^{\otimes M}$ , contract the input and first halves against $Q_i$ , retain second-half port $i$ , and sum over $i$ , where $\Phi_2=\frac12\sum_{x,y}|x,x\rangle\langle y,y|$ . Put

\nu_M=1-\operatorname{Re}(\mathcal P_M(|0\rangle\langle1|)_{0,1}), \qquad D_M(r)=\nu_M\left(\frac{1-r}{2}+\sqrt{1-r}\right), \quad J_i=(\operatorname{id}_2\otimes\mathcal E_i)(\Phi_2),

and

b_n=\frac{1-\frac12\|J_0^{\otimes n}-J_1^{\otimes n}\|_1}{2}, \qquad \|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}.

Let $p_n$ be the infimum of $(1-a_0+a_1)/2$ over adaptive tests with positive finite memory, an initial density matrix, a channel from memory-output back to memory-input at every step index, and a final effect $0\le H\le I$ ; a channel has a finite Kraus representation with $\sum_jK_j^\dagger K_j=I$ , and $a_i$ is the real trace of $H$ against the final state after $n$ uses of $\mathcal E_i$ and the prescribed intervening channels. Then

\frac{1-\frac n2(D_M(p)+D_M(q))-\sqrt{1-F^{2nM}}}{2} \le p_n\le b_n, \qquad \frac{1-\sqrt{1-F^{2n}}}{2}\le b_n\le\frac{F^n}{2}.

All endpoints $p,q=0,1$ are included, as is $p=q$ ; the tensor powers have entries given by products of the individual matrix entries.

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