Eqs.(24)–(26): explicit fidelity bounds

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.explicit_fidelity_lower_bounds

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

prove2quantum

For CPTP channels $\mathcal E_0,\mathcal E_1:d\to e$ , $d\ge2$ , $e\ge1$ , and $n\ge1$ , let $F$ be the root fidelity of their normalized Choi states, and let $B_M$ be the universal PBT bound. For every integer $M\ge2$ ,

B_M\ge\frac12-\frac12\sqrt{1-F^{2nM}}-\frac{d(d-1)n}{M}.

If $x>2$ and $M=xd(d-1)n$ is an admissible integer, this reads $B_M\ge1/2-1/x-\sqrt{1-F^{2nM}}/2$ , with $2nM=2xd(d-1)n^2$ . At the integer choice $M_*=4d(d-1)n$ ,

p_n\ge B_{M_*}\ge\frac{1-2\sqrt{1-F^{8d(d-1)n^2}}}{4}.

These explicit finite-use bounds retain the port-integrality requirement and require no assertion that a best finite port count exists.

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, (24)--(26): fidelity lower bounds at admissible INTEGER port
counts. The x-parametrization is used only when x*d*(d-1)*n is such an integer. -/
theorem explicit_fidelity_lower_bounds (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 F := rootFidelity (normalizedChannelChoi E0) (normalizedChannelChoi E1)
    (∀ M : ℕ, 2 ≤ M →
      1/2 - Real.sqrt (1-F^(2*n*M))/2 - (d : ℝ)*(d-1 : ℝ)*n/M ≤
        universalBound n M E0 E1) ∧
    (∀ (x : ℝ), 2 < x → ∀ M : ℕ, 2 ≤ M →
      (M : ℝ) = x*d*(d-1 : ℝ)*n →
      1/2 - 1/x - Real.sqrt (1-F^(2*n*M))/2 ≤ universalBound n M E0 E1) ∧
    ((1-2*Real.sqrt (1-F^(8*d*(d-1)*n^2)))/4 ≤
      universalBound n (4*d*(d-1)*n) E0 E1 ∧
      universalBound n (4*d*(d-1)*n) 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. 5, Eqs.(24)–(26): explicit fidelity bounds

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 channels $\mathcal E_0,\mathcal E_1:d\to e$ , where a channel is a finite Kraus map with $\sum_jK_j^\dagger K_j=I$ , put

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

For each $M$ , construct $\mathcal P_{d,M}$ from signals $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 effects $Q_i=RS_iR+M^{-1}(I-RSR)$ : apply these effects to the input and first halves of $M$ copies of $\Phi_d$ , retain second-half port $i$ , and sum over outcomes $i$ . Define

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

with the supremum over all matrices on two $d$ -dimensional registers and tensor-product entries given by products of the individual entries. Let $p_n$ be the infimum of $(1-a_0+a_1)/2$ over tests with a positive finite memory dimension, an initial density matrix on memory and input, a channel from memory and output back to memory and input at every natural step index, and a final effect $H$ satisfying $H\ge0$ and $I-H\ge0$ ; $a_i$ is the real trace of $H$ times the state obtained from $n$ applications of $\mathcal E_i$ , with the prescribed channels between them. Then, for every natural number $M\ge2$ ,

\frac12-\frac{\sqrt{1-F^{2nM}}}{2}-\frac{d(d-1)n}{M}\le B_{n,M}.

For every real $x>2$ and natural number $M\ge2$ satisfying $M=xd(d-1)n$ as an equality of real numbers,

\frac12-\frac1x-\frac{\sqrt{1-F^{2nM}}}{2}\le B_{n,M}.

Finally, for the natural number $M_*=4d(d-1)n$ ,

\frac{1-2\sqrt{1-F^{8d(d-1)n^2}}}{4} \le B_{n,M_*}\le p_n.

The condition involving $x$ is an implication and imposes no assertion that such an integer $M$ exists for each $x$ ; the real square root used throughout has value zero on negative arguments.

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