Nesting of fidelity-defined good and bad sets

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.good_bad_nesting

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

prove2quantum

Let $V$ be degraded from a binary cq channel $W$ by one CPTP map acting on both letter density operators, with finite nonempty output registers. Fix $0<\beta<1/2$ and $N=2^n$ . Define $\mathcal G_N(W,\beta)$ by the strict condition $\sqrt{F(W_N^{(i)})}<2^{-N^\beta}$ and let $\mathcal B_N$ be its complement. Then

\mathcal G_N(V,\beta)\subseteq\mathcal G_N(W,\beta),\qquad \mathcal B_N(W,\beta)\subseteq\mathcal B_N(V,\beta).

These inclusions compare the actual synthesized channels at every finite dyadic blocklength; they do not make the assistance set empty.

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, consequence of Lemma 3: both inclusions, with the source's operational beta range. -/
theorem good_bad_nesting {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 : ℕ) (beta : ℝ) (hpos : 0 < beta) (hbeta : beta < 1 / 2) :
    goodSet V n beta ⊆ goodSet W n beta ∧ badSet W n beta ⊆ badSet V n beta := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 4, §II, unnumbered consequence of Lemma 3: nesting of good and bad sets

Read-back

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

For finite, nonempty types $H,K$ with decidable equality, pairs $W_0,W_1$ and $V_0,V_1$ of positive semidefinite trace-one matrices on $H$ and $K$ , a map $D(X)=\sum_{a<r}L_aXL_a^\dagger$ for a finite family satisfying $\sum_aL_a^\dagger L_a=I_H$ , and the hypotheses $V_x=D(W_x)$ for both Boolean inputs, the following holds for every natural number $n$ , including $0$ , and every real $0<\beta<1/2$ . Put $\tau=2^{-(2^n)^\beta}$ . For either pair $Q=W,V$ , define $G_Q=\{i<2^n:f(Q_{n,i,0},Q_{n,i,1})<\tau\}$ and $B_Q=\{i<2^n:\tau\le f(Q_{n,i,0},Q_{n,i,1})\}$ , where $f(X,Y)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X}$ . Then

G_V\subseteq G_W\qquad\text{and}\qquad B_W\subseteq B_V.

For completeness, writing $N=2^n$ , the matrices used here have entries

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$ has $i$ Boolean entries and $h$ has $N$ entries in the relevant index type; $p(u)_k=\sum_j a_{jk}u_j\pmod2$ , and $a_{jk}=1$ exactly when every $1$ -bit of $k$ 's length- $n$ binary representation occurs at the reversed position in that of $j$ . Thus equality with the threshold belongs to $B_Q$ , and is excluded from $G_Q$ .

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