Theorem 15: polynomial Pauli channels and a modified-complement degrader

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.polynomialPauli_modifiedComplement

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

prove2quantum

Let $p_1,p_2,p_3$ be real polynomials with $p_i(0)=0$ . Put $p_0(t)=1-\sum_{i=1}^3p_i(t)$ , and assume these four weights form a probability distribution for every $t$ in a right neighborhood of zero. Let $c_i$ be the coefficient of $t$ in $p_i$ , set $C=|c_1c_2+c_1c_3+c_2c_3|$ , and let $N_t$ be the associated qubit Pauli channel with canonical Kraus-label complement. For every fixed choice of real $a_1,a_2,a_3$ satisfying $a_i=4\sum_{j\ne i}c_j$ whenever $c_i\ne0$ , define $q_i(t)=p_i(t+a_it^2)$ for $i=1,2,3$ and $q_0(t)=1-\sum_iq_i(t)$ . The $q_i(t)$ are physical eventually, and

\|N_t^c-N_{q(t)}^c\circ N_t\|_\diamond=O(t^2).

Independently, there are $K\ge0$ and $0<\delta\le1$ such that

\operatorname{dg}(N_t)\le256C t^2+Kt^3\qquad(0<t<\delta).

The constants may depend on the fixed polynomial family (and on the fixed $a_i$ for the first bound), but not on $t$ . When $c_i=0$ , $a_i$ is unrestricted, and the scalar bound includes $C=0$ . This retains both numbered conclusions (23) and (24).

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 15, PDF pp.16,20–21: polynomial evaluation in (22), arbitrary a_i
when c_i=0, and the sharp scalar bound (24) even when its coefficient is zero.
Source proof audit: the intermediate O(p^(5/2)) assertion at c_i=0 is not used
as a hypothesis or stated as a result; see MODERATION_NOTES.md. -/
theorem polynomialPauli_modifiedComplement (P : Fin 3 → Polynomial ℝ)
    (hP : PolynomialNoise P) :
    (∀ a : Fin 3 → ℝ,
      (∀ i, linearCoefficient P i ≠ 0 →
        a i = 4 * ∑ j ∈ Finset.univ.erase i, linearCoefficient P j) →
      ∃ K : ℝ, 0 ≤ K ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
        ∀ p ∈ Set.Ioo 0 delta,
          Probabilities (modifiedWeights P a p) ∧
          diamond (channelDifference (complementaryChannel (pauliDilation (polynomialWeights P p)))
            (complementaryChannel (pauliDilation (modifiedWeights P a p)) ∘
              receiverChannel (pauliDilation (polynomialWeights P p)))) ≤ K * p ^ 2) ∧
    (∃ K : ℝ, 0 ≤ K ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
      ∀ p ∈ Set.Ioo 0 delta,
        degradability (pauliDilation (polynomialWeights P p)) ≤
          256 * pairCoefficient P * 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. 16, Theorem 15: polynomial Pauli channels and a modified-complement degrader

Read-back

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

Let $P_0,P_1,P_2$ be real polynomials satisfying $P_i(0)=0$ , and suppose there exists $\delta_P>0$ such that the four numbers

w(p)=\bigl(1-P_0(p)-P_1(p)-P_2(p),P_0(p),P_1(p),P_2(p)\bigr)

are nonnegative and sum to $1$ for every $p\in[0,\delta_P]$ . Let $\ell_i$ be the coefficient of degree $1$ in $P_i$ , and put $b=|\ell_0\ell_1+\ell_0\ell_2+\ell_1\ell_2|$ . For any real four-vector $w$ , define $V(w)_{b,j;a}=\sqrt{w_j}(\sigma_j)_{ba}$ , using the identity and usual Pauli $X,Y,Z$ matrices, and set $N_w(X)=\operatorname{Tr}_{E}(V(w)XV(w)^\dagger)$ and $N_w^c(X)=\operatorname{Tr}_{B}(V(w)XV(w)^\dagger)$ . For every $a=(a_0,a_1,a_2)\in\mathbb R^3$ satisfying

\ell_i\ne0\ \Longrightarrow\ a_i=4\sum_{j\ne i}\ell_j,

there exist $K\ge0$ and $0<\delta\le1$ such that every $0<p<\delta$ gives nonnegative, sum-one modified weights

\widetilde w(p)=\bigl(1-\textstyle\sum_iP_i(p+a_ip^2),\ P_0(p+a_0p^2),P_1(p+a_1p^2),P_2(p+a_2p^2)\bigr)

and satisfies $\|N_{w(p)}^c-N_{\widetilde w(p)}^c\circ N_{w(p)}\|_\diamond\le Kp^2$ . No condition is imposed on $a_i$ when $\ell_i=0$ . In addition, there exist $K\ge0$ and $0<\delta\le1$ , separately quantified from those just described, such that every $0<p<\delta$ satisfies

\eta(V(w(p)))\le256\,b\,p^2+Kp^3.

Here $\eta(V)=\inf\{\eta\in[0,2]:\exists D\text{ a channel},\ \|N_V^c-D\circ N_V\|_\diamond\le\eta\}$ ; a channel is a finite Kraus sum with Kraus completeness $\sum_jK_j^\dagger K_j=I$ . For input space $H$ , $\|T\|_\diamond=\sup_{\|X\|_1\le1}\|(\operatorname{id}_{H}\otimes T)(X)\|_1$ , over arbitrary complex matrices on $H\times H$ , and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . The coefficient $b$ is the absolute value of the sum of the three products, and may be zero.

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