Complete attainable Pauli-damping region, including endpoints

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.attainable_complete

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

prove2quantum

Let $A_\gamma$ denote amplitude damping, $\chi_\gamma=(\mathrm{id}\otimes A_\gamma)(|\Phi^+\rangle\langle\Phi^+|)$ its normalized Choi state, and $P_q$ the Pauli map with Bloch action $(x,y,z)\mapsto(q_1x,-q_2y,q_3z)$ . For $0<\gamma<1$ , a qubit quantum channel $E$ is simulable by noisy Bell/Pauli teleportation over $\chi_\gamma$ if and only if

E=X^u\circ A_\eta\circ P_q,\qquad u\in\{0,1\},\quad0\le\eta\le\gamma,\quad q\in\operatorname{conv}(V_{\gamma,\eta}),

where $X$ denotes conjugation by the Pauli $X$ , $a=\sqrt{(1-\gamma)/(1-\eta)}$ , $b=1-\eta/\gamma$ , and the eight vertices are

V_{\gamma,\eta}=\{(a,\pm ab,\mp a^2b),(\pm ab,a,\mp a^2b),(-a,\pm ab,\pm a^2b),(\pm ab,-a,\pm a^2b)\}.

Signs within each triple are paired. At $\gamma=0$ the simulable channels are exactly all Pauli channels. At $\gamma=1$ they are exactly the input-independent diagonal states with Bloch vector $(0,0,z)$ , $-1\le z\le1$ . This characterizes the whole attainable set without asserting uniqueness of parameters.

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 pp.7--8, Theorem 16, converse paragraph and vertex proof.
Corrected endpoint clauses use the physical simulator rather than undefined 0/0 vertices.
No decomposition uniqueness is asserted. -/
theorem attainable_complete :
    (∀ gamma : ℝ, 0 < gamma → gamma < 1 → ∀ E : QubitMap, IsChannel E →
      (Simulable (normalizedQubitChoi (blochAmplitudeDamping gamma)) E ↔
        ∃ u : Bool, ∃ eta : ℝ, ∃ q : BlochCoordinates,
          0 ≤ eta ∧ eta ≤ gamma ∧ q ∈ attainableRegion gamma eta ∧
          E = pauliDamping u eta q)) ∧
    (∀ E : QubitMap, IsChannel E →
      (Simulable (normalizedQubitChoi (blochAmplitudeDamping 0)) E ↔ IsPauli E)) ∧
    (∀ E : QubitMap, IsChannel E →
      (Simulable (normalizedQubitChoi (blochAmplitudeDamping 1)) E ↔
        ∃ z : ℝ, -1 ≤ z ∧ z ≤ 1 ∧ E = axialReplacement z)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 7, Theorem 16, Eqs.(59)–(67)

Read-back

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

Write $\sigma_0=I_2,\sigma_1=X,\sigma_2=Y,\sigma_3=Z$ ; every complex qubit matrix has a unique expression $R=(tI_2+r_0X+r_1Y+r_2Z)/2$ , with complex coefficients. Define

D_\gamma(R)=\tfrac12[tI_2+\sqrt{1-\gamma}\,r_0X+\sqrt{1-\gamma}\,r_1Y+((1-\gamma)r_2+\gamma t)Z], \quad \tau_\gamma=(\mathrm{id}\otimes D_\gamma)(|\Omega\rangle\langle\Omega|), \quad |\Omega\rangle=(|00\rangle+|11\rangle)/\sqrt2.

Here an extension $\mathrm{id}\otimes E$ applies $E$ to each block indexed by the first qubit. For a two-qubit matrix $\tau$ , put $\beta_k(c,a)=2^{-1/2}(\sigma_k)_{ac}$ and define $T_{\tau,p}$ by

[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'), \qquad T_{\tau,p}(R)=\sum_{k,\ell=0}^3p_{\ell k}\sigma_\ell K_{\tau,k}(R)\sigma_\ell^\dagger.

To be simulable from $\tau$ means that $E=T_{\tau,p}$ for some real array with $p_{\ell k}\ge0$ and $\sum_\ell p_{\ell k}=1$ for every $k$ . A channel here means a map having a finite representation $E(R)=\sum_hA_hRA_h^\dagger$ , with $\sum_hA_h^\dagger A_h=I_2$ , on all complex qubit matrices. The theorem asserts the conjunction of three statements. First, for every $0<\gamma<1$ and every channel $E$ , simulability from $\tau_\gamma$ is equivalent to the existence of $u\in\{\mathrm{false},\mathrm{true}\}$ , $\eta\in\mathbb R$ , and $q\in\mathbb R^3$ such that $0\le\eta\le\gamma$ , $q$ belongs to the convex hull of

(a,ab,-a^2b),\ (a,-ab,a^2b),\ (ab,a,-a^2b),\ (-ab,a,a^2b),\ (-a,ab,a^2b),\ (-a,-ab,-a^2b),\ (ab,-a,a^2b),\ (-ab,-a,-a^2b), \quad a=\sqrt{\frac{1-\gamma}{1-\eta}},\quad b=1-\frac{\eta}{\gamma},

and $E(R)=X^uD_\eta(P_q(R))X^u$ for every $R$ , where $X^{\mathrm{false}}=I_2$ , $X^{\mathrm{true}}=X$ , and $P_q(R)=(tI_2+q_0r_0X-q_1r_1Y+q_2r_2Z)/2$ . Second, for every channel $E$ , simulability from $\tau_0$ is equivalent to $E(R)=\sum_hw_h\sigma_hR\sigma_h^\dagger$ for some real $w_h\ge0$ summing to $1$ . Third, for every channel $E$ , simulability from $\tau_1$ is equivalent to the existence of a real $z\in[-1,1]$ such that $E(R)=\operatorname{tr}(R)(I_2+zZ)/2$ for every $R$ .

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