Eq.(36), Methods IV.C: exact amplitude-damping simulation error

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.amplitude_damping_simulation_error

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

prove2quantum

Let $p\in[0,1]$ , integer $M\ge2$ , and let $\xi_M$ be the standard qubit PBT number. For the actual channel $\mathcal E_p$ with excited state $|1\rangle$ decaying to $|0\rangle$ , set $\mathcal E_p^M=\mathcal E_p\circ\Gamma_{2,M}$ . Its unhalved diamond error is

\|\mathcal E_p-\mathcal E_p^M\|_\diamond=\xi_M\left(\frac{1-p}{2}+\sqrt{1-p}\right).

This makes the channel-specific bound computable. The supporting Choi calculation corrects the second diagonal in printed Eq. (59) from $(1-p)\xi_M$ to $(1-p)\xi_M/4$ , as required by the Kraus action and unit trace; independent moderation of this correction is pending.

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.7, (36), Methods p.9: actual diamond simulation error.
Source correction in supporting (59): printed second diagonal (1-p)*xi
must be (1-p)*xi/4, as forced by applying (33) to (57) and unit trace.
This correction requires independent moderation. -/
theorem amplitude_damping_simulation_error (M : ℕ) (hM : 2 ≤ M)
    (p : ℝ) (hp : p ∈ Set.Icc 0 1) :
    diamond (fun X => amplitudeDampingChannel p X -
      simulated (amplitudeDampingChannel p) M X) = dampingSimulationError M p := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 7, Eq.(36), Methods IV.C: exact amplitude-damping simulation error

Read-back

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

For every natural number $M\ge2$ and real number $p\in[0,1]$ , let

\mathcal A_p(X)= \begin{pmatrix}1&0\\0&\sqrt{1-p}\end{pmatrix} X \begin{pmatrix}1&0\\0&\sqrt{1-p}\end{pmatrix} + \begin{pmatrix}0&\sqrt p\\0&0\end{pmatrix} X \begin{pmatrix}0&0\\\sqrt p&0\end{pmatrix}.

Construct the qubit port map $\mathcal P_M$ by setting $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}$ and $f(0)=0$ , and $Q_i=RS_iR+M^{-1}(I-RSR)$ ; on $X\otimes\Phi_2^{\otimes M}$ , where $\Phi_2=\frac12\sum_{x,y}|x,x\rangle\langle y,y|$ , contract the input and first halves against $Q_i$ , retain second-half port $i$ , and sum over $i$ . Write $\nu_M=1-\operatorname{Re}(\mathcal P_M(|0\rangle\langle1|)_{0,1})$ , and define

\Delta_2(\mathcal F)= \sup_{\|X\|_1\le1}\|(\operatorname{id}_2\otimes\mathcal F)(X)\|_1, \qquad \|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X},

where $X$ ranges over all matrices on two qubits. Then the error of the composed simulation is exactly

\Delta_2(\mathcal A_p-\mathcal A_p\circ\mathcal P_M) =\nu_M\left(\frac{1-p}{2}+\sqrt{1-p}\right).

The parameter values $p=0$ and $p=1$ 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