Diamond distance dominates unassisted channel trace distance

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.diamond_dominatesTrace

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

prove2quantum

Let $E_1,E_2$ be trace-preserving completely positive maps from a qubit to a qubit. Define the unassisted distance by the supremum of $\|E_1(\rho)-E_2(\rho)\|_1$ over normalized qubit density matrices. Define the diamond distance by the same supremum after applying $\mathrm{id}_2\otimes E_i$ to normalized two-qubit density matrices. Then

\|E_1-E_2\|_\diamond\ge\|E_1-E_2\|_1.

Both norms are full trace norms, without a factor of one half. This compares assisted and unassisted channel distinguishability.

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, Lemma 25: two actual qubit channels,
normalized density inputs and the full trace norm on both sides. -/
theorem diamond_dominatesTrace (E F : QubitMap) (hE : IsChannel E) (hF : IsChannel F) :
    channelTraceDistance E F ≤ channelDiamondDistance E F := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 14, Lemma 25

Read-back

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

For every two maps $E,F:M_2(\mathbb C)\to M_2(\mathbb C)$ , assume each has a finite Kraus representation: for each $G\in\{E,F\}$ , there are a natural number $m_G$ and matrices $K_{G,0},\ldots,K_{G,m_G-1}\in M_2(\mathbb C)$ such that $\sum_jK_{G,j}^{*}K_{G,j}=I_2$ and $G(X)=\sum_jK_{G,j}XK_{G,j}^{*}$ for every matrix $X$ . Then

\sup_{\substack{\rho\in M_2(\mathbb C)\\ \rho\succeq0,\ \operatorname{tr}\rho=1}} \operatorname{tr}\sqrt{(E(\rho)-F(\rho))^{*}(E(\rho)-F(\rho))} \ \le\ \sup_{\substack{\rho\in M_4(\mathbb C)\\ \rho\succeq0,\ \operatorname{tr}\rho=1}} \operatorname{tr}\sqrt{D_\rho^{*}D_\rho}, \qquad D_\rho=(\operatorname{id}_2\otimes E)(\rho)-(\operatorname{id}_2\otimes F)(\rho).

Here $\operatorname{id}_2\otimes G$ applies $G$ to each $2\times2$ block of a matrix indexed by a pair of Boolean indices, leaving the first index as the block index; the square roots are the positive semidefinite matrix square roots. Neither supremum includes a factor of $1/2$ .

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