General noisy-teleportation channel

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.noisyTeleport_general

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

prove2quantum

Let $\tau$ be any positive semidefinite two-qubit matrix of trace one. Fix the Bell outcomes $(\Phi^+,\Psi^+,\Psi^-,\Phi^-)$ , the corrections $(I,X,Y,Z)$ , and a conditional law $p(l\mid k)\ge0$ with $\sum_l p(l\mid k)=1$ for each $k$ . The resource and law are independent of the input, and every Bell branch is retained. Write $b_i=\operatorname{Tr}[(I\otimes\sigma_i)\tau]$ and $t_{ji}=\operatorname{Tr}[(\sigma_j\otimes\sigma_i)\tau]$ for $i,j=1,2,3$ . Define $t'_{0i}=b_i$ and $t'_{ji}=t_{ji}$ for $j>0$ . The resulting operation is a quantum channel with Bloch action

r'_i=f_{i0}+\sum_{j=1}^3 f_{ij}r_j,\qquad f_{ij}=t'_{ji}S_{ij},\qquad S_{ij}=\frac14\sum_{k,l=0}^3(-1)^{\delta_{k0}+\delta_{j2}+\delta_{j0}+\delta_{kj}+\delta_{il}+\delta_{0l}}p(l\mid k).

Here $i=1,2,3$ , $j=0,1,2,3$ , $\delta$ is the Kronecker delta, and $r$ is any Bloch vector with $\|r\|_2\le1$ . This identifies the full affine channel produced by the physical 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.5, Theorem 11 and Eqs.(37)--(39).
The physical Bell instrument is characterized; no affine-form hypothesis is assumed. -/
theorem noisyTeleport_general (tau : ResourceOp) (htau : IsDensityMatrix tau)
    (p : Fin 4 → Fin 4 → ℝ) (hp : ClassicalTeleportationLaw p) :
    IsChannel (noisyTeleport tau p) ∧ noisyTeleport tau p =
      QAlgorithms.QubitChannels.blochAffineMap
        (fun i => fCoordinate tau p i 0)
        (fun i j => fCoordinate tau p i j.succ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 5, Theorem 11, Eqs.(37)–(39)

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$ , where $X,Y,Z$ are the usual Pauli matrices, and let Boolean indices label the two coordinates of a qubit. For every positive semidefinite matrix $\tau$ on two qubits with $\operatorname{tr}\tau=1$ , and every real array $p_{\ell k}$ , $k,\ell\in\{0,1,2,3\}$ , satisfying $p_{\ell k}\ge0$ and $\sum_\ell p_{\ell k}=1$ for each $k$ , define $\beta_k(c,a)=2^{-1/2}(\sigma_k)_{ac}$ , the maps

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

and, for $i\in\{0,1,2\}$ , $j\in\{0,1,2,3\}$ , define

m_{ji}=\operatorname{Re}\operatorname{tr}[(\sigma_j\otimes\sigma_{i+1})\tau], \quad s_{ij}=\frac14\sum_{k,\ell=0}^3 (-1)^{\delta_{k0}+\delta_{j2}+\delta_{j0}+\delta_{kj}+\delta_{i+1,\ell}+\delta_{0\ell}}p_{\ell k}, \quad f_{ij}=m_{ji}s_{ij},

where $\delta_{ab}=1$ if $a=b$ and $0$ otherwise. Then $T_{\tau,p}$ has a finite Kraus representation: there exist $m\in\mathbb N$ and qubit matrices $E_0,\ldots,E_{m-1}$ with $\sum_hE_h^\dagger E_h=I_2$ and $T_{\tau,p}(R)=\sum_hE_hRE_h^\dagger$ for every complex qubit matrix $R$ . Moreover, on every such $R$ ,

T_{\tau,p}(R) =\frac{\operatorname{tr}R}{2}\left(I_2+\sum_{i=0}^2 f_{i0}\sigma_{i+1}\right) +\frac12\sum_{i=0}^2 \left(\sum_{j=0}^2f_{i,j+1}\operatorname{tr}(\sigma_{j+1}R)\right)\sigma_{i+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