Eq.(27): finite square-root bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.nearby_channels_square_root

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

prove2quantum

Let $\mathcal E_0,\mathcal E_1:d\to e$ be CPTP, with $d\ge2$ , $e\ge1$ , and $n\ge1$ . Set $\epsilon=1-F(\rho_{\mathcal E_0},\rho_{\mathcal E_1})$ , the exact normalized-Choi root infidelity, so $0\le\epsilon\le1$ , and choose integer $M_*=4d(d-1)n$ . Then

p_n\ge B_{M_*}\ge\frac14-n\sqrt{2d(d-1)\epsilon}.

Here $p_n$ is the equal-prior optimal adaptive discrimination error, and $B_M$ the unclipped PBT expression. This is the exact finite square-root inequality of Eq. (27), separated from the source's unquantified exponential approximation.

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 p.5, exact first inequality of (27): epsilon is the EXACT Choi
infidelity. The following approximate exponential is separately deferred. -/
theorem nearby_channels_square_root (d e n : ℕ) [NeZero d] [NeZero e]
    (hd : 2 ≤ d) (hn : 1 ≤ n) (E0 E1 : Superop (Fin d) (Fin e))
    (h0 : IsChannel E0) (h1 : IsChannel E1) :
    let epsilon := 1-rootFidelity (normalizedChannelChoi E0) (normalizedChannelChoi E1)
    epsilon ∈ Set.Icc 0 1 ∧
    1/4 - n * Real.sqrt (2*(d : ℝ)*(d-1 : ℝ)*epsilon) ≤
      universalBound n (4*d*(d-1)*n) E0 E1 ∧
    1/4 - n * Real.sqrt (2*(d : ℝ)*(d-1 : ℝ)*epsilon) ≤ 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. 5, Eq.(27): finite square-root bound

Read-back

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

For all natural numbers $d,e,n$ , equipped with $d,e\ne0$ , with $d\ge2$ and $n\ge1$ , and all finite Kraus channels $\mathcal E_0,\mathcal E_1:d\to e$ whose Kraus operators satisfy $\sum_jK_j^\dagger K_j=I$ , let

\Phi_d=\frac1d\sum_{x,y}|x,x\rangle\langle y,y|, \qquad J_i=(\operatorname{id}_d\otimes\mathcal E_i)(\Phi_d), \qquad \varepsilon=1-\operatorname{Re}\operatorname{tr}\sqrt{\sqrt{J_0}J_1\sqrt{J_0}}.

To define the bound, construct the port map $\mathcal P_{d,M}$ using signal entries $S_i[(x,a),(y,b)]=d^{-1}\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}$ and $f(0)=0$ , and $Q_i=RS_iR+M^{-1}(I-RSR)$ : on $X\otimes\Phi_d^{\otimes M}$ , contract the input and first halves against $Q_i$ , retain the second half of port $i$ , and sum over $i$ . Put

\epsilon_{d,M} =\sup_{\|X\|_1\le1} \|(\operatorname{id}_d\otimes(\operatorname{id}-\mathcal P_{d,M}))(X)\|_1, \qquad B_{n,M}= \frac{1-n\epsilon_{d,M}-\frac12\|J_0^{\otimes nM}-J_1^{\otimes nM}\|_1}{2},

where $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , the supremum ranges over arbitrary matrices on two input registers, and tensor-product entries are products of the individual entries. Let $p_n$ be the infimum of $(1-a_0+a_1)/2$ over adaptive tests having positive finite memory, a density matrix as initial memory-input state, channels from memory-output to memory-input at every step index, and a final effect $0\le H\le I$ ; $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

0\le\varepsilon\le1, \qquad \frac14-n\sqrt{2d(d-1)\varepsilon} \le B_{n,\,4d(d-1)n}, \qquad \frac14-n\sqrt{2d(d-1)\varepsilon}\le p_n.

This includes $\varepsilon=0$ and $\varepsilon=1$ ; no strict closeness condition is assumed.

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