Largest attainable diamond distance from Pauli channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.maximalPauliDistance

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

prove2quantum

Fix $0\le\gamma\le1$ and the normalized amplitude-damping Choi state $\chi_\gamma$ . Every channel $E$ simulated over this resource by a conditional classical law in the Bell/Pauli protocol admits a Pauli channel $P$ satisfying

\|E-P\|_\diamond\le\gamma.

Let $E_*$ be the physical protocol that ignores Alice's classical label and always applies $I$ . There is a Pauli channel $P_*$ with $\|E_*-P_*\|_\diamond=\gamma$ , and every Pauli $P$ satisfies $\gamma\le\|E_*-P\|_\diamond$ . Thus the largest attainable distance is achieved and equals $\gamma$ , including both endpoints. All distances use the full trace norm with a normalized qubit reference.

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.10: upper bound for every attainable channel and
attainment by always applying I; gamma=0 and gamma=1 are retained. -/
theorem maximalPauliDistance (gamma : ℝ) (h0 : 0 ≤ gamma) (h1 : gamma ≤ 1) :
    (∀ p : Fin 4 → Fin 4 → ℝ, ClassicalTeleportationLaw p →
      ∃ F : QubitMap, IsPauli F ∧
        channelDiamondDistance (noisyTeleport (normalizedQubitChoi (blochAmplitudeDamping gamma)) p) F ≤ gamma) ∧
    (∃ F : QubitMap, IsPauli F ∧
      channelDiamondDistance
        (noisyTeleport (normalizedQubitChoi (blochAmplitudeDamping gamma)) discardClassical) F = gamma) ∧
    (∀ F : QubitMap, IsPauli F → gamma ≤ channelDiamondDistance
      (noisyTeleport (normalizedQubitChoi (blochAmplitudeDamping gamma)) discardClassical) F) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 10, Consequence following Proposition 19

Read-back

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

For every real $\gamma\in[0,1]$ , define $D_\gamma$ on arbitrary complex matrices $R=(tI_2+r_0X+r_1Y+r_2Z)/2$ by

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

Let $(\sigma_0,\sigma_1,\sigma_2,\sigma_3)=(I_2,X,Y,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'), \qquad T_p(R)=\sum_{k,\ell=0}^3p_{\ell k}\sigma_\ell K_{\tau_\gamma,k}(R)\sigma_\ell^\dagger.

Call a map $F$ a Pauli mixture when $F(R)=\sum_hw_h\sigma_hR\sigma_h^\dagger$ for all $R$ , for some real $w_h\ge0$ summing to $1$ . Define $d_\diamond(G,H)$ as the supremum of $\operatorname{tr}\sqrt{D_\rho^\dagger D_\rho}$ over positive semidefinite two-qubit matrices $\rho$ of trace $1$ , with $D_\rho=(\mathrm{id}\otimes G)(\rho)-(\mathrm{id}\otimes H)(\rho)$ ; the extensions apply the maps to blocks indexed by the first qubit, and no factor $1/2$ is included. The theorem asserts all three of the following: for every real array $p_{\ell k}\ge0$ whose columns sum to $1$ , there exists a Pauli mixture $F$ with $d_\diamond(T_p,F)\le\gamma$ ; for the particular array $p^*_{\ell k}=1$ when $\ell=0$ and $0$ otherwise, there exists a Pauli mixture $F$ with $d_\diamond(T_{p^*},F)=\gamma$ ; and every Pauli mixture $F$ satisfies $\gamma\le d_\diamond(T_{p^*},F)$ . The assertions include both $\gamma=0$ and $\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