§4 unnumbered main result: quadratic degradability for generalized qudit Pauli channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.quditPauli_quadraticDegradability

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

prove2quantum

Fix an integer dimension $d\ge1$ . In the standard basis define $X|j\rangle=|j+1\pmod d\rangle$ and $Z|j\rangle=e^{2\pi i j/d}|j\rangle$ . For any probability distribution $w_{k\ell}$ on $0\le k,\ell<d$ , let $N_w(\rho)=\sum_{k,\ell}w_{k\ell}X^kZ^\ell\rho(X^kZ^\ell)^\dagger$ and use its canonical Kraus-label dilation. There exist $C_d\ge0$ and $0<\delta_d\le2$ such that, uniformly over $w$ ,

\|N_w-\mathrm{id}_d\|_\diamond\le\varepsilon\le\delta_d \quad\Longrightarrow\quad \operatorname{dg}(N_w)\le C_d\varepsilon^2\qquad(\varepsilon\ge0).

The degradability parameter optimizes the full diamond error over all CPTP degrading maps. This is the stated class-level improvement for generalized Pauli noise; no polynomial-family hypothesis or dimension-independent constant is imposed.

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)

/-- §4 unnumbered main result, PDF pp.12,19: dimension-dependent but channel-uniform
quadratic bound for ALL generalized Pauli probability distributions near identity. -/
theorem quditPauli_quadraticDegradability (d : ℕ) (hd : 0 < d) :
    ∃ C : ℝ, 0 ≤ C ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 2 ∧
      ∀ w : (Fin d × Fin d) → ℝ, Probabilities w →
      ∀ eps ∈ Set.Icc 0 delta,
        diamond (channelDifference (receiverChannel (quditPauliDilation d w)) id) ≤ eps →
        degradability (quditPauliDilation d w) ≤ C * eps ^ 2 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 12, §4 unnumbered main result: quadratic degradability for generalized qudit Pauli channels

Read-back

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

For every positive integer $d$ , there are real constants $C\ge0$ and $0<\delta\le2$ with the following property. Index the standard basis of $\mathbb C^d$ by $0,\ldots,d-1$ , let $S_{ij}=1$ when $i=j+1\pmod d$ and $0$ otherwise, and let $Z_{jj}=e^{2\pi\mathrm{i}j/d}$ . For every collection of real weights $w_{rs}\ge0$ with $\sum_{r,s}w_{rs}=1$ , define

V_{b,(r,s);a}=\sqrt{w_{rs}}\,(S^rZ^s)_{ba},\qquad N_V(X)=\operatorname{Tr}_{E}(VXV^\dagger),\qquad N_V^c(X)=\operatorname{Tr}_{B}(VXV^\dagger).

Here both $B$ and the input have dimension $d$ , and $E$ is indexed by the $d^2$ pairs $(r,s)$ . For a matrix map $T$ with input index set $H$ , write

\|T\|_\diamond=\sup_{\|X\|_1\le1}\|(\operatorname{id}_{H}\otimes T)(X)\|_1,

where $X$ ranges over all complex matrices on $H\times H$ , without positivity or Hermiticity restrictions, and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . Define

\eta(V)=\inf\{\eta\in[0,2]:\exists D:B\to E\text{ a channel},\ \|N_V^c-D\circ N_V\|_\diamond\le\eta\},

where a channel means a map $X\mapsto\sum_jK_jXK_j^\dagger$ with finitely many Kraus matrices satisfying $\sum_jK_j^\dagger K_j=I$ . Then every $\varepsilon\in[0,\delta]$ satisfies

\|N_V-\operatorname{id}\|_\diamond\le\varepsilon \quad\Longrightarrow\quad \eta(V)\le C\varepsilon^2.

The constants are chosen before the weights and $\varepsilon$ ; the assertion includes $d=1$ and $\varepsilon=0$ .

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