Degradation and both monotonicities survive synthesis

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.degradation_preserved

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

prove2quantum

Let $W$ and $V$ be binary-input cq channels with density outputs on finite nonempty registers. Suppose one CPTP map $D$ satisfies $V(x)=D(W(x))$ for both input letters. For $N=2^n$ and each synthesized index $i$ , retain the previous classical bits and apply $D^{\otimes N}$ to the quantum outputs. This constructed map $D_{N,i}$ is CPTP and satisfies

V_N^{(i)}(x)=D_{N,i}(W_N^{(i)}(x)),\qquad I(V_N^{(i)})\le I(W_N^{(i)}),\qquad F(W_N^{(i)})\le F(V_N^{(i)}).

Here $I$ is symmetric Holevo information in bits and $F$ is squared Uhlmann fidelity. No commutation or complementary-channel hypothesis is required. This supplies the degradation interface for the polar index sets.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P10

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P10

open scoped BigOperators Matrix ComplexConjugate

open Filter

-- Accepted definitions, without paper-local aliases.

open QAlgorithms.Papers.Independent.Information100.P58 (basisDensity)

open QAlgorithms.Papers.Independent.Information100.P67 (squaredFidelity)

open QAlgorithms.Papers.Independent.Claimed50.P48 (indexedKrausDilation)

/-- PDF p.4, Lemma 3: the constructed degrading map is CPTP, maps both synthesized
letters correctly, and gives both Holevo-information and SQUARED-fidelity inequalities. -/
theorem degradation_preserved {H K : Type*} [Fintype H] [DecidableEq H] [Nonempty H]
    [Fintype K] [DecidableEq K] [Nonempty K]
    (W : BinaryCQ H) (V : BinaryCQ K) (hW : IsBinaryCQ W) (hV : IsBinaryCQ V)
    (D : Superop H K) (hD : IsChannel D) (hdeg : ∀ x, V x = D (W x))
    (n : ℕ) (i : Fin (2 ^ n)) :
    IsChannel (synthesizedDegrader D n i) ∧
    (∀ x, synthesized V n i x = synthesizedDegrader D n i (synthesized W n i x)) ∧
    symmetricInformation (synthesized V n i) ≤ symmetricInformation (synthesized W n i) ∧
    squaredFidelity (synthesized W n i false) (synthesized W n i true) ≤
      squaredFidelity (synthesized V n i false) (synthesized V n i true) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 4, Lemma 3: degradation is preserved by synthesis

Read-back

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

Let $H,K$ be finite, nonempty types with decidable equality; let $W_0,W_1$ and $V_0,V_1$ be positive semidefinite trace-one matrices on $H$ and $K$ , respectively; and let $D$ be a function admitting a finite Kraus representation $D(X)=\sum_{a<r}L_aXL_a^\dagger$ , with $\sum_aL_a^\dagger L_a=I_H$ , such that $V_x=D(W_x)$ for both Boolean inputs $x$ . For every natural number $n$ , including $0$ , and every index $i<2^n$ , put $N=2^n$ and define, for either matrix pair $Q=W,V$ ,

Q_{n,i,x}((v,h),(v',h'))= \begin{cases} 2^{-(N-1)}\displaystyle\sum_{\substack{u\in\{0,1\}^N\\u_i=x,\ u_{<i}=v}} \prod_{k<N}Q_{p(u)_k}(h_k,h'_k),&v=v',\\ 0,&v\ne v', \end{cases}

where $v\in\{0,1\}^i$ , $h$ is a length- $N$ word over the relevant index type, and $p(u)_k=\sum_j a_{jk}u_j\pmod2$ , with $a_{jk}=1$ exactly when each $1$ -bit of $k$ 's length- $n$ binary representation is present at the reversed position in that of $j$ . Define a map $\mathcal D$ on these registers by

\mathcal D(X)((v,k),(v',k'))= \sum_{h,h'\in H^N}X((v,h),(v',h')) \prod_{t<N}D(E_{h_t,h'_t})(k_t,k'_t),

where $E_{a,b}$ is the matrix with entry $1$ at $(a,b)$ and zero elsewhere. The conclusion is the conjunction that $\mathcal D$ itself admits a finite Kraus representation with completeness sum equal to the identity, that $V_{n,i,x}=\mathcal D(W_{n,i,x})$ for both $x$ , and that

I(V_{n,i})\le I(W_{n,i}),\qquad f(W_{n,i,0},W_{n,i,1})^2\le f(V_{n,i,0},V_{n,i,1})^2.

Here $f(X,Y)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X}$ , $I(Q)=S((Q_0+Q_1)/2)-(S(Q_0)+S(Q_1))/2$ , and $S(X)=-\operatorname{Re}\operatorname{tr}[(t\mapsto t\log_2t)(X)]$ , interpreted by continuous functional calculus with the value $0\log_2 0=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