Bell-diagonal resources yield only Pauli channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.bellDiagonal_onlyPauli

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

prove2quantum

Let $w_0,\ldots,w_3\ge0$ sum to one and let $\tau=\sum_k w_k|B_k\rangle\langle B_k|$ , with the Bell ordering $(\Phi^+,\Psi^+,\Psi^-,\Phi^-)$ . For every conditional stochastic law $p(l\mid k)$ , the branch-averaged Bell-measurement protocol with Pauli corrections simulates a channel $E$ for which there is a normalized probability law $v$ satisfying

E(\rho)=\sum_{l=0}^3 v_l\sigma_l\rho\sigma_l^\dagger\quad\text{for every density matrix }\rho.

Here $(\sigma_0,\sigma_1,\sigma_2,\sigma_3)=(I,X,Y,Z)$ . Thus arbitrary classical noise cannot turn a Bell-diagonal resource into a non-Pauli channel.

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.6, Theorem 12: all normalized Bell mixtures and
all conditional stochastic channels, without a doubly-stochastic restriction. -/
theorem bellDiagonal_onlyPauli (w : Fin 4 → ℝ) (hw : FourOutcomeLaw w)
    (p : Fin 4 → Fin 4 → ℝ) (hp : ClassicalTeleportationLaw p) :
    IsPauli (noisyTeleport (teleportationBellMixture w) p) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 6, Theorem 12

Read-back

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

Let $\sigma_0=I_2,\sigma_1=X,\sigma_2=Y,\sigma_3=Z$ , and define two-qubit vectors by $\beta_k(c,a)=2^{-1/2}(\sigma_k)_{ac}$ for Boolean $c,a$ . For every real vector $w=(w_0,\ldots,w_3)$ with $w_k\ge0$ and $\sum_kw_k=1$ , form the matrix $\tau$ with entries $\tau_{(c,a),(d,a')}=\sum_kw_k\beta_k(c,a)\overline{\beta_k(d,a')}$ . For every real array $p_{\ell k}$ with $p_{\ell k}\ge0$ and $\sum_\ell p_{\ell k}=1$ for each $k$ , define

[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.

There exists a real vector $v=(v_0,\ldots,v_3)$ satisfying $v_h\ge0$ and $\sum_hv_h=1$ such that $T_{\tau,p}(R)=\sum_{h=0}^3v_h\sigma_hR\sigma_h^\dagger$ for every complex qubit matrix $R$ ; zero weights are permitted in both $w$ and $v$ .

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