§II.J, Eq.(35): amplitude-damping Choi fidelity

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.amplitude_damping_choi_fidelity

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

prove2quantum

Let $p,q\in[0,1]$ and let $\mathcal E_p$ be the qubit amplitude-damping channel with $K_0=|0\rangle\langle0|+\sqrt{1-p}|1\rangle\langle1|$ and $K_1=\sqrt p|0\rangle\langle1|$ . For normalized reference-first Choi states,

F(\rho_{\mathcal E_p},\rho_{\mathcal E_q})=\frac{1+\sqrt{(1-p)(1-q)}+\sqrt{pq}}2.

Here $F$ is root fidelity. This gives the explicit overlap entering both the adaptive lower bound and the Bell-probe block bounds.

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, (32)--(35): Choi ROOT fidelity for the frozen actual
amplitude-damping channel, excited |1> decaying to |0>. -/
theorem amplitude_damping_choi_fidelity (p q : ℝ)
    (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) :
    rootFidelity (normalizedChannelChoi (amplitudeDampingChannel p))
      (normalizedChannelChoi (amplitudeDampingChannel q)) = dampingFidelity p q := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 7, §II.J, Eq.(35): amplitude-damping Choi fidelity

Read-back

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

For every pair of real numbers $p,q\in[0,1]$ , define maps on complex $2\times2$ matrices by

\mathcal A_p(X)=K_{p,0}XK_{p,0}^\dagger+K_{p,1}XK_{p,1}^\dagger, \qquad K_{p,0}=\begin{pmatrix}1&0\\0&\sqrt{1-p}\end{pmatrix}, \quad K_{p,1}=\begin{pmatrix}0&\sqrt p\\0&0\end{pmatrix},

and similarly for $q$ . With $\Phi_2=\frac12\sum_{i,j=0}^1|i,i\rangle\langle j,j|$ and $J_p=(\operatorname{id}_2\otimes\mathcal A_p)(\Phi_2)$ , their root fidelity satisfies

\operatorname{Re}\operatorname{tr}\sqrt{\sqrt{J_p}J_q\sqrt{J_p}} =\frac{1+\sqrt{(1-p)(1-q)}+\sqrt{pq}}2.

Both endpoints of each parameter interval are included.

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