Fast polarization toward poor commuting-output channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.fastPolarization_poor

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

prove2quantum

Let $W:x\mapsto\rho_x$ be a binary cq channel on a finite nonempty register, and suppose $\rho_0\rho_1=\rho_1\rho_0$ . For $N=2^n$ , synthesize channels with the prescribed polar transform and let $f_i=\sqrt{F(W_N^{(i)})}$ . For every real $\beta<1/2$ ,

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

The strict inequality uses root fidelity. Uniform counting is the marginal probability of the fair synthesis process. This result supplies poor-channel polarization under commuting outputs and requires no degradation assumption.

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 pp.4–5, Proposition 4: strict poor threshold for ROOT fidelity; degradation
is not a hypothesis. Counting leaves is the independent fair birth-process marginal. -/
theorem fastPolarization_poor {H : Type*} [Fintype H] [DecidableEq H] [Nonempty H]
    (W : BinaryCQ H) (hW : IsBinaryCQ W) (hc : Commute (W false) (W true))
    (beta : ℝ) (hbeta : beta < 1 / 2) :
    Tendsto (fun n => leafProbability (poorSet W n beta)) atTop
      (nhds (1 - symmetricInformation W)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 4, Proposition 4: fast polarization toward poor commuting channels

Read-back

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

Let $H$ be a finite, nonempty set with decidable equality, and let $W_0,W_1$ be positive semidefinite complex matrices indexed by $H$ , each having trace $1$ , such that $W_0W_1=W_1W_0$ . Let $\beta\in\mathbb R$ satisfy $\beta<\tfrac12$ ; no positivity assumption on $\beta$ is imposed. Write $S(X)=-\operatorname{Re}\operatorname{tr}(f(X))$ , where $f(t)=t\log_2t$ is applied by continuous functional calculus, and put $I(W)=S((W_0+W_1)/2)-(S(W_0)+S(W_1))/2$ . The matrices used to define the asserted limit are as follows. For $n\in\mathbb N$ , put $N=2^n$ , and let $d_t(j)$ denote bit $t$ , counted from the most significant end, of the $n$ -bit representation of $0\le j<N$ . Set $c_{jk}=1$ exactly when, for every $0\le t<n$ , $d_t(k)=1$ implies $d_{n-1-t}(j)=1$ , and otherwise set $c_{jk}=0$ . For a Boolean word $u$ of length $N$ , define $v_k(u)=\sum_{j=0}^{N-1}u_jc_{jk}\pmod2$ , interpreting Boolean values as $0,1$ . For $0\le i<N$ and $x\in\{0,1\}$ , define a matrix $W_{n,i}^{(x)}$ , indexed by pairs $(h,a)$ with $h\in\{0,1\}^i$ and $a\in H^N$ , by

W_{n,i}^{(x)}((h,a),(h',b)) = \begin{cases} 2^{-(N-1)} \displaystyle\sum_{\substack{u\in\{0,1\}^N\\u_i=x,\;u_{<i}=h}} \prod_{k=0}^{N-1}W_{v_k(u)}(a_k,b_k),&h=h',\\ 0,&h\ne h'. \end{cases}

For matrices of the same size, put $F_{\mathrm r}(X,Y)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X}$ , with square roots taken by continuous functional calculus. Then

\lim_{n\to\infty} \frac{\#\{\,0\le i<2^n: 1-2^{-(2^n)^\beta}<F_{\mathrm r}(W_{n,i}^{(0)},W_{n,i}^{(1)})\,\}}{2^n} =1-I(W).

The defining sequence includes $n=0$ : then $N=1$ , the bit condition is vacuous, the transformed word is unchanged, and there is one synthesized index.

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