Explicit nearest Pauli channel in the full trace norm

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.nearestPauli_trace

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

prove2quantum

Let $T=\operatorname{conv}\{(1,-1,1),(1,1,-1),(-1,-1,-1),(-1,1,1)\}$ , $q\in T$ , $0\le\eta\le1$ , and $u\in\{0,1\}$ . Let $P_q(x,y,z)=(q_1x,-q_2y,q_3z)$ , let $A_\eta$ be amplitude damping, and put $E=X^u\circ A_\eta\circ P_q$ , where $X$ denotes Pauli conjugation. Define $C$ by deleting the translation of $E$ : its actual Bloch diagonal is $(\sqrt{1-\eta}q_1,-\sqrt{1-\eta}q_2,(1-\eta)q_3)$ when $u=0$ and $(\sqrt{1-\eta}q_1,\sqrt{1-\eta}q_2,-(1-\eta)q_3)$ when $u=1$ . Then $C$ is a Pauli channel and

\|E-C\|_1=\eta,\qquad\eta\le\|E-P\|_1\quad\text{for every Pauli channel }P,

where $\|E-F\|_1=\sup_{\rho\ge0,\,\operatorname{Tr}\rho=1}\|E(\rho)-F(\rho)\|_1$ uses the full matrix trace norm. This gives explicit attainment, without claiming that the minimizer is unique.

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 pp.9,14, Proposition 18: explicit attainment and
comparison against every Pauli competitor, with full trace norm and no uniqueness. -/
theorem nearestPauli_trace (u : Bool) (eta : ℝ) (h0 : 0 ≤ eta) (h1 : eta ≤ 1)
    (q : BlochCoordinates) (hq : q ∈ pauliTetrahedron) :
    IsPauli (closestPauli u eta q) ∧
    channelTraceDistance (pauliDamping u eta q) (closestPauli u eta q) = eta ∧
    ∀ F : QubitMap, IsPauli F → eta ≤ channelTraceDistance (pauliDamping u eta q) F := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 9, Proposition 18

Read-back

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

For every Boolean $u$ , every real $\eta$ with $0\le\eta\le1$ , and every $q=(q_0,q_1,q_2)$ in the convex hull of $(1,-1,1),(1,1,-1),(-1,-1,-1),(-1,1,1)$ , set $a=\sqrt{1-\eta}$ and $\epsilon_u=1$ when $u=\mathrm{false}$ , $\epsilon_u=-1$ when $u=\mathrm{true}$ . Define maps on arbitrary complex qubit matrices $R=(tI_2+r_0X+r_1Y+r_2Z)/2$ by

E(R)=\tfrac12[tI_2+aq_0r_0X-\epsilon_u aq_1r_1Y+ \epsilon_u((1-\eta)q_2r_2+\eta t)Z], \quad C(R)=\tfrac12[tI_2+aq_0r_0X-\epsilon_u aq_1r_1Y+ \epsilon_u(1-\eta)q_2r_2Z].

For any maps $G,H$ , let $d_{\mathrm{tr}}(G,H)$ be the supremum of $\operatorname{tr}\sqrt{(G(\rho)-H(\rho))^\dagger(G(\rho)-H(\rho))}$ over all positive semidefinite qubit matrices $\rho$ of trace $1$ ; this definition contains no factor $1/2$ . Then $C$ is a Pauli mixture, meaning $C(R)=\sum_{h=0}^3w_h\sigma_hR\sigma_h^\dagger$ for every $R$ , with real $w_h\ge0$ , $\sum_hw_h=1$ , and $(\sigma_0,\sigma_1,\sigma_2,\sigma_3)=(I_2,X,Y,Z)$ . Moreover, $d_{\mathrm{tr}}(E,C)=\eta$ , and $\eta\le d_{\mathrm{tr}}(E,F)$ for every map $F$ having such a Pauli-mixture representation. Both endpoints $\eta=0,1$ and all boundary points of the stated convex hull 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