The same channel minimizes full diamond distance

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.nearestPauli_diamond

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 Pauli and

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

Here the diamond distance is the supremum of the full output trace norm over normalized density matrices of a qubit input and a qubit reference, with the identity acting on the reference. The same explicit channel attains both minima, independently of a resource realization or uniqueness of the decomposition.

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--10,14--15, Proposition 19: the same explicit
channel attains the diamond minimum; the reference is a normalized qubit state. -/
theorem nearestPauli_diamond (u : Bool) (eta : ℝ) (h0 : 0 ≤ eta) (h1 : eta ≤ 1)
    (q : BlochCoordinates) (hq : q ∈ pauliTetrahedron) :
    IsPauli (closestPauli u eta q) ∧
    channelDiamondDistance (pauliDamping u eta q) (closestPauli u eta q) = eta ∧
    ∀ F : QubitMap, IsPauli F → eta ≤ channelDiamondDistance (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 19

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 let $\epsilon_u=1$ for $u=\mathrm{false}$ and $-1$ for $u=\mathrm{true}$ . Define, for every complex qubit matrix $R=(tI_2+r_0X+r_1Y+r_2Z)/2$ ,

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 maps $G,H$ , define $d_\diamond(G,H)$ as the supremum, over positive semidefinite two-qubit matrices $\rho$ of trace $1$ , of $\operatorname{tr}\sqrt{D_\rho^\dagger D_\rho}$ , where $D_\rho=(\mathrm{id}\otimes G)(\rho)-(\mathrm{id}\otimes H)(\rho)$ and each extension applies its map to the blocks indexed by the first qubit. This uses a qubit reference and contains no factor $1/2$ . Then $C$ has a representation $C(R)=\sum_{h=0}^3w_h\sigma_hR\sigma_h^\dagger$ on all $R$ , where $(\sigma_0,\sigma_1,\sigma_2,\sigma_3)=(I_2,X,Y,Z)$ , $w_h\ge0$ , and $\sum_hw_h=1$ . Furthermore, $d_\diamond(E,C)=\eta$ , and every map $F$ with such a Pauli-mixture representation satisfies $\eta\le d_\diamond(E,F)$ . The quantifiers include $\eta=0,1$ and the entire boundary of the stated convex hull.

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