Pauli dephasing has a classical environment in an unbiased basis

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.dephasing_classical_environment

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

prove2quantum

Let $0\le p\le1$ , let $\sigma\in\{X,Y,Z\}$ , and use the dilation $V|\psi\rangle=\sqrt{1-p}|\psi\rangle|0\rangle+\sqrt p\sigma|\psi\rangle|1\rangle$ . Choose an orthonormal input basis with $\langle\psi_x|\sigma|\psi_x\rangle=0$ for both letters. The complementary outputs are

\operatorname{Tr}_B(V|\psi_x\rangle\langle\psi_x|V^\dagger)=\operatorname{diag}(1-p,p),\qquad x\in\{0,1\},

so they commute. The computational basis for $X$ noise and the Hadamard basis for $Z$ noise give these outputs explicitly as well. The zero-expectation criterion includes $Y$ and avoids using the Pauli eigenbasis.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P10

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P10

open scoped BigOperators Matrix ComplexConjugate

open Filter

-- Accepted definitions, without paper-local aliases.

open QAlgorithms.Papers.Independent.Information100.P58 (basisDensity)

open QAlgorithms.Papers.Independent.Information100.P67 (squaredFidelity)

open QAlgorithms.Papers.Independent.Claimed50.P48 (indexedKrausDilation)

/-- PDF p.11, Appendix B: the zero-Pauli-expectation (bit-flipping) basis criterion
includes X,Y,Z. Both complement letters equal diag(1-p,p), hence commute.
The source's X computational-basis and Z Hadamard-basis examples are included explicitly. -/
theorem dephasing_classical_environment (p : ℝ) (hlo : 0 ≤ p) (hhi : p ≤ 1)
    (sigma : Matrix Bool Bool ℂ) (hsigma : sigma = pauliX ∨ sigma = pauliY ∨ sigma = pauliZ)
    (basis : Matrix.unitaryGroup Bool ℂ)
    (hunbiased : ∀ x : Bool,
      inner ℂ (basisColumn basis x) (act sigma (basisColumn basis x)) = 0) :
    (∀ x : Bool, dephasingComplement p sigma (pureDensity (basisColumn basis x)) =
      dephasingDiagonal p) ∧
    Commute (dephasingComplement p sigma (pureDensity (basisColumn basis false)))
      (dephasingComplement p sigma (pureDensity (basisColumn basis true))) ∧
    (∀ x : Bool, dephasingComplement p pauliX (basisDensity x) = dephasingDiagonal p) ∧
    (∀ x : Bool, dephasingComplement p pauliZ (pureDensity (act hadamard (ket x))) =
      dephasingDiagonal p) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 11, Appendix B, unnumbered dephasing-channel classical-environment example

Read-back

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

For every $p\in[0,1]$ , every matrix $\sigma$ equal to one of

X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad Y=\begin{pmatrix}0&-\mathrm i\\\mathrm i&0\end{pmatrix},\qquad Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix},

and every unitary matrix $U$ indexed by false and true whose columns $u_x$ satisfy $\langle u_x,\sigma u_x\rangle=0$ for each $x$ , define $\mathcal C_{p,\sigma}(\rho)_{b,c}=\operatorname{tr}(K_b\rho K_c^\dagger)$ , where $K_0=\sqrt{1-p}\,I$ , $K_1=\sqrt p\,\sigma$ , and $0,1$ denote false,true. Then $\mathcal C_{p,\sigma}(u_xu_x^\dagger)=D_p=\operatorname{diag}(1-p,p)$ for each $x$ , and the two outputs for $x=0,1$ commute. In addition, for each $x\in\{0,1\}$ ,

\mathcal C_{p,X}(|x\rangle\langle x|)=D_p,\qquad \mathcal C_{p,Z}\bigl((H|x\rangle)(H|x\rangle)^\dagger\bigr)=D_p, \quad H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix},

where $|x\rangle$ has amplitude one at $x$ and zero at the other index. The endpoints $p=0,1$ are included.

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