Theorem 17: sharper equal-error XZ degradability expansion

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.xz_degradability_expansion

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

prove2quantum

Let $C_p$ be the qubit channel with independent X and Z errors, each of probability $p$ :

C_p(\rho)=(1-p)^2\rho+(p-p^2)X\rho X+p^2Y\rho Y+(p-p^2)Z\rho Z.

Use the canonical four-label dilation. There exist $K\ge0$ and $0<\delta\le1$ such that

\operatorname{dg}(C_p)\le16p^2+32p^{5/2}+Kp^3\qquad(0<p<\delta).

The degradability parameter minimizes full diamond error over CPTP degrading maps. The fractional-power term is part of the sharper asserted expansion.

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 17, PDF p.17: retains the fractional-power 32 p^(5/2) term.
The canonical XZ dilation has independent equal X and Z error probabilities p. -/
theorem xz_degradability_expansion :
    ∃ K : ℝ, 0 ≤ K ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
      ∀ p ∈ Set.Ioo 0 delta,
        degradability (xzDilation p) ≤
          16 * p ^ 2 + 32 * p ^ (5 / 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. 17, Theorem 17: sharper equal-error XZ degradability expansion

Read-back

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

For real $p$ , define $w(p)=((1-p)^2,p-p^2,p^2,p-p^2)$ and $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}$ , where $\sigma_0,\sigma_1,\sigma_2,\sigma_3$ are the identity and usual Pauli $X,Y,Z$ matrices. Set $N_p(X)=\operatorname{Tr}_E(V_pXV_p^\dagger)$ , $N_p^c(X)=\operatorname{Tr}_B(V_pXV_p^\dagger)$ , and

\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 is a finite Kraus sum $D(X)=\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ . For a map with input space $H$ , its diamond quantity is $\sup_{\|X\|_1\le1}\|(\operatorname{id}_H\otimes T)(X)\|_1$ , over arbitrary complex matrices on $H\times H$ , where $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . There exist real $K\ge0$ and $0<\delta\le1$ such that every $0<p<\delta$ satisfies

\eta(V_p)\le16p^2+32p^{5/2}+Kp^3.

The exponent $5/2$ is a real exponent, and neither endpoint $p=0,\delta$ is 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