Theorem 13: improved depolarizing degradability coefficient

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.depolarizing_degradability_expansion

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

prove2quantum

For $0\le p\le1$ , define the qubit depolarizing channel $D_p(\rho)=(1-p)\rho+\frac p3(X\rho X+Y\rho Y+Z\rho Z)$ , using the canonical dilation with Kraus labels $I,X,Y,Z$ . Thus $p$ is the total Pauli error. There exist $K\ge0$ and $0<\delta\le1$ such that

\operatorname{dg}(D_p)\le\frac89(6+\sqrt2)p^2+Kp^3\qquad(0<p<\delta).

Here $\operatorname{dg}$ minimizes full diamond error over all CPTP degrading maps. This retains the improved depolarizing coefficient rather than the rough preliminary bound.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P50

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P50

variable {A B E F : Type}

variable [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B]

variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]

open QAlgorithms.Papers.Independent.Information100.P67
  (IsIsometry receiverChannel complementaryChannel maximumCoherentInformation
    dilationPower idealJoint)

open QAlgorithms.Papers.Independent.Information100.P80 (log2)

open QAlgorithms.Papers.Independent.Information100.P69 (diamond choi)

open QAlgorithms.Papers.Independent.Support50.P07 (fullTracePrivateCapacity)

open QAlgorithms.Papers.Independent.Frontier18.P17 (clock)

/-- Theorem 13, PDF pp.13–15: improved 8/9(6+sqrt 2) coefficient and cubic
remainder; p is total Pauli error. -/
theorem depolarizing_degradability_expansion :
    ∃ K : ℝ, 0 ≤ K ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
      ∀ p ∈ Set.Ioo 0 delta,
        degradability (depolarizingDilation p) ≤
          (8 / 9 : ℝ) * (6 + Real.sqrt 2) * p ^ 2 + K * p ^ 3 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 13, Theorem 13: improved depolarizing degradability coefficient

Read-back

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

Let $\sigma_0=I$ , $\sigma_1=\begin{pmatrix}0&1\\1&0\end{pmatrix}$ , $\sigma_2=\begin{pmatrix}0&-\mathrm{i}\\\mathrm{i}&0\end{pmatrix}$ , and $\sigma_3=\operatorname{diag}(1,-1)$ . For real $p$ , define $w(p)=(1-p,p/3,p/3,p/3)$ and the matrix $V_p:\mathbb C^2\to\mathbb C^2\otimes\mathbb C^4$ by $(V_p)_{b,j;a}=\sqrt{w_j(p)}(\sigma_j)_{ba}$ . Put $N_p(X)=\operatorname{Tr}_{\mathbb C^4}(V_pXV_p^\dagger)$ and $N_p^c(X)=\operatorname{Tr}_{\mathbb C^2}(V_pXV_p^\dagger)$ , and define

\eta(V_p)=\inf\{\eta\in[0,2]:\exists D:\mathbb C^2\to\mathbb C^4\text{ a channel},\ \|N_p^c-D\circ N_p\|_\diamond\le\eta\}.

A channel has a finite Kraus representation $D(X)=\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ ; the diamond quantity is $\sup_{\|X\|_1\le1}\|(\operatorname{id}\otimes T)(X)\|_1$ , with a reference register of the input dimension and arbitrary complex $X$ , and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . There exist real $K\ge0$ and $0<\delta\le1$ such that, for every $0<p<\delta$ ,

\eta(V_p)\le \frac89(6+\sqrt2)\,p^2+Kp^3.

The parameter range excludes $p=0$ and $p=\delta$ .

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