Amplitude damping cannot teleport itself except at endpoints

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.amplitudeDamping_selfSimulation

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

prove2quantum

For $0\le\gamma\le1$ , let $A_\gamma$ be amplitude damping and $\chi_\gamma$ its normalized two-qubit Choi state. In the fixed Bell-measurement protocol with Pauli corrections and arbitrary conditional classical communication,

A_\gamma\text{ is simulable over }\chi_\gamma\quad\Longleftrightarrow\quad\gamma\in\{0,1\}.

Thus self-simulation fails for $0<\gamma<1$ . Identity teleportation realizes the zero endpoint, and a correction supported on $I,Z$ realizes the reset channel at one. The assertion concerns this specified noisy-teleportation protocol.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P13

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P13

attribute [local instance] Classical.propDecidable Classical.decEq

/-- arXiv:1706.05384v2 PDF p.8, paragraph following Theorem 16.
Both printed exceptions are included positively; this is only the Bell/Pauli protocol. -/
theorem amplitudeDamping_selfSimulation (gamma : ℝ) (h0 : 0 ≤ gamma) (h1 : gamma ≤ 1) :
    Simulable (normalizedQubitChoi (blochAmplitudeDamping gamma)) (blochAmplitudeDamping gamma) ↔
      gamma = 0 ∨ gamma = 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 8, Consequence following Theorem 16

Read-back

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

For every real $\gamma$ with $0\le\gamma\le1$ , let $D_\gamma$ be the map sending an arbitrary complex matrix $R=(tI_2+r_0X+r_1Y+r_2Z)/2$ to

D_\gamma(R)=\tfrac12[tI_2+\sqrt{1-\gamma}\,r_0X+\sqrt{1-\gamma}\,r_1Y+((1-\gamma)r_2+\gamma t)Z],

and set $\tau_\gamma=(\mathrm{id}\otimes D_\gamma)(|\Omega\rangle\langle\Omega|)$ , where $|\Omega\rangle=(|00\rangle+|11\rangle)/\sqrt2$ and the extension applies $D_\gamma$ to each block indexed by the first qubit. Put $\sigma_0=I_2,\sigma_1=X,\sigma_2=Y,\sigma_3=Z$ , $\beta_k(c,a)=2^{-1/2}(\sigma_k)_{ac}$ , and

[K_{\tau,k}(R)]_{bb'}=\sum_{c,a,d,a'\in\{0,1\}} \overline{\beta_k(c,a)}R_{cd}\tau_{(a,b),(a',b')}\beta_k(d,a').

There exists a real array $p_{\ell k}\ge0$ with $\sum_\ell p_{\ell k}=1$ for every $k$ and

D_\gamma(R)=\sum_{k,\ell=0}^3p_{\ell k}\sigma_\ell K_{\tau_\gamma,k}(R)\sigma_\ell^\dagger \quad\text{for every complex qubit matrix }R

if and only if $\gamma=0$ or $\gamma=1$ .

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