Necessary resource condition for non-Pauli simulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.nonPauli_resourceNecessary

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

prove2quantum

Let $\tau$ be a normalized two-qubit density matrix and fix any conditional stochastic law in the noisy Bell/Pauli protocol. Write $b_i=\operatorname{Tr}[(I\otimes\sigma_i)\tau]$ for Bob's local Bloch vector and $T_{ij}=\operatorname{Tr}[(\sigma_i\otimes\sigma_j)\tau]$ for its correlations. If the simulated channel is not a normalized mixture of Pauli conjugations, then

b\ne0\quad\text{or}\quad\exists i\ne j:\ T_{ij}\ne0.

Moreover $\tau\ne(\mathrm{id}\otimes P)(|\Phi^+\rangle\langle\Phi^+|)$ for every Pauli channel $P$ . This necessary condition constrains Bob's vector, and imposes no condition on Alice's local Bloch vector.

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, Corollary 13: Bob's vector or off-diagonal
correlations are necessary; also excludes every normalized Pauli Choi resource. -/
theorem nonPauli_resourceNecessary (tau : ResourceOp) (htau : IsDensityMatrix tau)
    (p : Fin 4 → Fin 4 → ℝ) (hp : ClassicalTeleportationLaw p)
    (hnon : ¬ IsPauli (noisyTeleport tau p)) :
    (bobVector tau ≠ 0 ∨ ∃ i j : Fin 3, i ≠ j ∧ resourcePauliCorrelation tau i j ≠ 0) ∧
    ∀ w : Fin 4 → ℝ, FourOutcomeLaw w → tau ≠ normalizedQubitChoi (pauliMixture w) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 6, Corollary 13

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 put $\beta_k(c,a)=2^{-1/2}(\sigma_k)_{ac}$ for Boolean indices. For every positive semidefinite two-qubit matrix $\tau$ of trace $1$ , and every real array $p_{\ell k}\ge0$ with $\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.

Suppose there is no real vector $v$ with $v_h\ge0$ , $\sum_hv_h=1$ , and $T_{\tau,p}(R)=\sum_hv_h\sigma_hR\sigma_h^\dagger$ for every complex qubit matrix $R$ . Then the vector $(\operatorname{Re}\operatorname{tr}[(I_2\otimes\sigma_{i+1})\tau])_{i=0}^2$ is nonzero, or there exist distinct $i,j\in\{0,1,2\}$ with $\operatorname{Re}\operatorname{tr}[(\sigma_{i+1}\otimes\sigma_{j+1})\tau]\ne0$ . In addition, for every real vector $w$ satisfying $w_h\ge0$ and $\sum_hw_h=1$ ,

\tau\ne(\mathrm{id}\otimes P_w)(|\Omega\rangle\langle\Omega|), \qquad P_w(R)=\sum_{h=0}^3w_h\sigma_hR\sigma_h^\dagger, \qquad |\Omega\rangle=\frac{|00\rangle+|11\rangle}{\sqrt2},

where $\mathrm{id}\otimes P_w$ applies $P_w$ to each block indexed by the first qubit.

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