Fast polarization toward good cq channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.fastPolarization_good

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

prove2quantum

Let $W:x\mapsto\rho_x$ be a binary-input cq channel with density operators on a finite nonempty quantum register. Write $I(W)=H((\rho_0+\rho_1)/2)-(H(\rho_0)+H(\rho_1))/2$ , where $H$ is von Neumann entropy in bits. For $N=2^n$ , form all $N$ synthesized channels using the row transform $G_N=B_NF_2^{\otimes n}$ , and let $f_i=\sqrt{F(W_N^{(i)})}$ be their root fidelities. For every real $\beta<1/2$ ,

\lim_{n\to\infty}\frac{1}{2^n}\left|\left\{i:f_i<2^{-(2^n)^\beta}\right\}\right|=I(W).

Uniform choice among the synthesized leaves has exactly the marginal law of the independent fair-branch channel birth process. Thus this is the source's probability-limit assertion, including $\beta\le0$ .

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.3, Theorem 2: fair-branch marginal probability, expressed as uniform
counting over all 2^n synthesized leaves. The full printed beta range is retained. -/
theorem fastPolarization_good {H : Type*} [Fintype H] [DecidableEq H] [Nonempty H]
    (W : BinaryCQ H) (hW : IsBinaryCQ W) (beta : ℝ) (hbeta : beta < 1 / 2) :
    Tendsto (fun n => leafProbability (goodSet W n beta)) atTop
      (nhds (symmetricInformation W)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 3, Theorem 2: fast polarization toward good cq channels

Read-back

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

For every finite, nonempty type $H$ with decidable equality, every pair $W_0,W_1$ of positive semidefinite $H$ -indexed complex matrices of trace $1$ , and every real $\beta<1/2$ , the following limit holds:

\lim_{n\to\infty} \frac{\left|\left\{i<2^n:f(W_{n,i,0},W_{n,i,1})<2^{-(2^n)^\beta}\right\}\right|}{2^n} = S\!\left(\frac{W_0+W_1}{2}\right)-\frac{S(W_0)+S(W_1)}2.

Here $f(X,Y)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X}$ , and $S(X)=-\operatorname{Re}\operatorname{tr}\bigl[(t\mapsto t\log_2t)(X)\bigr]$ , using continuous functional calculus and the total real logarithm, so the contribution at $t=0$ is $0$ . To define $W_{n,i,x}$ , put $N=2^n$ , let $p(u)_k=\sum_j a_{jk}u_j\pmod2$ , and set $a_{jk}=1$ exactly when every $1$ -bit of $k$ 's length- $n$ binary representation occurs at the reversed position in that of $j$ . Its entries, indexed by $v\in\{0,1\}^i$ and $h\in H^N$ , are

W_{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}W_{p(u)_k}(h_k,h'_k),&v=v',\\ 0,&v\ne v'. \end{cases}

No positive lower bound on $\beta$ is assumed: zero and negative values are 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