Successive cancellation reliability, including the finite bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.reliability

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

prove2quantum

Let $\mathcal N:A'\to BE$ be a memoryless finite-register quantum wiretap channel with qubit input, with a fixed isometric extension $V:A'\to BES_2$ . Choose two unit purifications $|\psi_z\rangle^{A'S_1}$ of the input states, with $z\in\{0,1\}$ equiprobable. Both shields $S_1,S_2$ are excluded from Eve. Let $W_{A,B}$ and $W_{A,E}$ be the resulting amplitude channels to Bob and Eve. The virtual phase channel $W_{P,B}$ has output $BCS_1S_2$ , obtained by phase modulating the reference of the coherent source $2^{-1/2}\sum_z|z\rangle^C|\psi_z\rangle$ and tracing only Eve after $V$ . Entropies and Holevo information are in bits, and $F$ denotes squared fidelity.

Fix $0<\beta<1/2$ and blocklength $N=2^n$ . Use Arikan's fixed transform $G_N$ for amplitude and its transpose for phase; amplitude splitting reveals previous bits and averages future bits, while phase splitting reveals future bits and averages previous bits. An index is good precisely when its synthesized root fidelity is strictly less than $2^{-N^\beta}$ . Write $\mathcal G_A,\mathcal G_P$ for the good sets and define $\mathcal A=\mathcal G_A\cap\mathcal G_P$ , $\mathcal X=\mathcal G_A\setminus\mathcal G_P$ , $\mathcal Z=\mathcal G_P\setminus\mathcal G_A$ , and $\mathcal B=[N]\setminus(\mathcal G_A\cup\mathcal G_P)$ . The code sends independent uniform private bits on $\mathcal A$ , local random bits on $\mathcal X$ , frozen bits known to Bob on $\mathcal Z$ , and preshared uniform secret key bits on $\mathcal B$ . Error and leakage average over these uniform choices.

Let $\mathcal C=\mathcal A\cup\mathcal X$ . There is a family of quantum successive cancellation POVMs on $B^N$ , indexed by the known frozen and key bits and chosen independently of the unknown input bits, that decodes every bit in $\mathcal C$ . Its average block error obeys

\Pr\{\widehat U_{\mathcal C}\ne U_{\mathcal C}\} \le b_n:=\sqrt{2\sum_{i\in\mathcal C}\sqrt{F(W_{A,B,N}^{(i)})}}, \qquad b_n=o\!\left(2^{-N^\beta/2}\right).

The sequential decoder uses a binary projective test at each decoded index, adapting to the previous decisions; frozen indices require no test. This is a reliability statement for both information and locally randomized bits.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P74

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P74

open QAlgorithms

open scoped ComplexConjugate Matrix

noncomputable section

local instance (p : Prop) : Decidable p := Classical.propDecidable p

variable {B E S1 S2 : Type}

variable [Fintype B] [Fintype E] [Fintype S1] [Fintype S2]

variable [DecidableEq B] [DecidableEq E] [DecidableEq S1] [DecidableEq S2]

/-- PDF p.4, §II.D: one input-independent POVM family recovers A union X using the
frozen/key bits. Both the finite bound and the printed little-o claim are retained.
The elementary cutoff estimate alone does not prove the latter; it is not assumed. -/
theorem reliability (d : WiretapData B E S1 S2) (hd : d.Valid)
    (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    ∃ M : (n : ℕ) → PolarDecoderEffects d beta n,
      (∀ n, IsSuccessiveCancellation d beta n (M n)) ∧
      (∀ n k, IsPOVM (M n k)) ∧
      (∀ n, decoderError d beta n (M n) ≤ reliabilityBound d beta n) ∧
      Asymptotics.IsLittleO Filter.atTop (reliabilityBound d beta) (decayHalf beta) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 4, §II.D, unnumbered: quantum successive cancellation reliability

Read-back

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

For finite index types $B,E,S_1,S_2$ , with decidable equality as required, let $d=(V,\psi)$ satisfy $V^*V=I_2$ and $\|\psi_z\|=1$ for both Boolean $z$ , and let $0<\beta<\tfrac12$ . Define

s_z(b,e,s,t)=\sum_{a\in\{0,1\}}V_{(b,e,t),a}\psi_z(a,s),\qquad W_z=\operatorname{Tr}_{E,S_1,S_2}(s_zs_z^*).

For each natural $n$ , including zero, put $N=2^n$ , $I=\{0,\ldots,N-1\}$ , let $G_{ij}=1$ precisely when every bit $k<n$ set in $j$ has bit $n-1-k$ set in $i$ , and set $e(u)_j=\sum_i u_iG_{ij}\pmod2$ . For $J_i=\{j:j<i\}$ , define

[\Sigma_{i,b}]_{(h,y),(h',y')}= \begin{cases} 2^{-(N-1)} \displaystyle\sum_{\substack{u\in\{0,1\}^I\\u_i=b,\ u|_{J_i}=h}} \prod_{\ell\in I}W_{e(u)_\ell}(y_\ell,y'_\ell),&h=h',\\ 0,&h\ne h', \end{cases}

and put

F(R,S)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt R\,S\sqrt R},\qquad D_n=\{i:F(\Sigma_{i,0},\Sigma_{i,1})<2^{-N^\beta}\},\qquad R_n=\sqrt{2\sum_{i\in D_n}F(\Sigma_{i,0},\Sigma_{i,1})}.

There exists a family $M_n(k,m)$ of complex matrices on $B^I$ , indexed by assignments $k:I\setminus D_n\to\{0,1\}$ and $m:D_n\to\{0,1\}$ , with all of the following properties. For each $n$ , there are matrices $T_{k,i,h}$ for every $k,i$ , and every history $h:J_i\to\{0,1\}$ , such that $T_{k,i,h}$ and $I-T_{k,i,h}$ are positive semidefinite and $T_{k,i,h}^2=T_{k,i,h}$ ; if $u$ is assembled from $k,m$ , set

P_i= \begin{cases} T_{k,i,u|_{J_i}},&i\in D_n,\ u_i=0,\\ I-T_{k,i,u|_{J_i}},&i\in D_n,\ u_i=1,\\ I,&i\notin D_n, \end{cases} \qquad K=P_{N-1}\cdots P_0; \quad M_n(k,m)=K^*K.

For every $n,k$ , the matrices $M_n(k,m)$ are positive semidefinite and sum over $m$ to the identity. Their error satisfies

2^{-N}\sum_{u\in\{0,1\}^I} \left[ 1-\operatorname{Re}\operatorname{tr} \left( M_n(u|_{I\setminus D_n},u|_{D_n}) \bigotimes_{i\in I}W_{e(u)_i} \right) \right]\le R_n \quad\text{for every }n.

Finally $R_n=o(2^{-N^\beta/2})$ as $n\to\infty$ : for every $c>0$ , eventually $|R_n|\le c\,2^{-N^\beta/2}$ . Empty decoded sets and empty histories are included, with the corresponding empty sums and products.

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