Coherent polar encoding polarizes the phase channel

Open

QAlgorithms.Papers.Independent.Intakethird100.P23.phase_polarization

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

prove2quantum

Let $U:\mathbb C^2\to\mathbb C^b\otimes\mathbb C^e$ be an isometry, so $U^\dagger U=I$ , defining a memoryless channel to Bob and its fixed complementary channel to Eve. All binary inputs are uniform and entropies are in bits. At recursion depth $n\ge0$ , let $N=2^n$ and apply the coherent Arikan encoder $G_N=B_NF^{\otimes n}$ , where $F=\left(\begin{smallmatrix}1&0\\1&1\end{smallmatrix}\right)$ . Amplitude synthesis retains previous bits and averages future bits; phase synthesis retains future bits and averages previous bits, with Bob's coherent copy register $C^N$ retained. Write $r(W)=\|\sqrt{\rho_0}\sqrt{\rho_1}\|_1=\sqrt{F(W)}$ for the root fidelity of a binary channel $W$ . Fix $0<\beta<1/2$ and put $t_n=2^{-N^\beta}$ . Let $G_A,G_P,G_E$ be the respective amplitude-good, phase-good, and Eve-amplitude-good sets, with the strict rule $r(W_N^{(i)})<t_n$ . Write $\mathcal A=G_A\cap G_P$ and $\mathcal B=(G_A\cup G_P)^c$ . Each set depends on $n$ and $\beta$ .

The physical encoded purification for a phase string $x$ is

|\sigma_{x,N}\rangle=2^{-N/2}\sum_{z\in\{0,1\}^N}(-1)^{x\cdot z}|\phi_{zG_N}\rangle^{B^NE^N}|z\rangle^{C^N}.

Construct the synthesized phase channels from its $B^NC^N$ marginal with the reverse history convention above. If $I(W_P)$ is the single-use phase channel's symmetric Holevo information, then

\lim_{n\to\infty}\frac{|G_P|}{2^n}=I(W_P).

This identifies the asymptotic supply of phase-good positions for the coding scheme.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P23

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P23

open scoped BigOperators ComplexConjugate Matrix

open Filter

open QAlgorithms (Qubits)

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

attribute [local instance] Classical.propDecidable

/-- Phase polarization for the actual Eq.(8) vector and reverse side information
(I.B, PDF pp.2–3); the limit is along N=2^n. -/
theorem phase_polarization {b e : ℕ} (U : Matrix (Fin b × Fin e) Bool ℂ)
    (hU : Uᴴ * U = 1) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    Tendsto (fun n => indexRate (goodPhase U n beta)) atTop (nhds (phaseInformation U)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P23

Source

Quantum polar codes for arbitrary channels, arXiv:1201.2906v2, PDF p. 3, I.B, Eq. (8)

Read-back

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

For all natural numbers $b,e$ , every complex matrix $U$ with rows indexed by $\{0,\ldots,b-1\}\times\{0,\ldots,e-1\}$ and Boolean columns satisfying $U^\dagger U=I_2$ , and every real $\beta$ satisfying $0<\beta<\tfrac12$ , the following convergence holds. Identify Boolean values with $0,1$ . For each natural number $n$ , including $0$ , set $N=2^n$ and define a binary matrix $G^{(n)}$ by

G^{(n)}_{rj}=1 \quad\Longleftrightarrow\quad \forall\,0\le k<n,\ \left\lfloor\frac{j}{2^k}\right\rfloor\bmod2 \le \left\lfloor\frac{r}{2^{n-1-k}}\right\rfloor\bmod2,

with entry zero otherwise, and define $p_n(u)_j=(\sum_{r=0}^{N-1}u_rG^{(n)}_{rj})\bmod2$ . Define vectors and matrices

w_x(\mathbf r,u,\mathbf z) = 2^{-N/2}(-1)^{\sum_jx_ju_j} \prod_{j=0}^{N-1}U_{(r_j,z_j),p_n(u)_j}, \qquad Q_n(x)=\operatorname{Tr}_{\mathbf z}|w_x\rangle\langle w_x|.

Thus $Q_n(x)$ is indexed by pairs $(\mathbf r,u)$ . For $i<N$ , let $m_i^+(x)$ be the full length- $N$ bit string whose $j$ -th bit is $x_j$ when $i<j$ , and zero otherwise, and put

P_{n,i}(a) = 2^{-(N-1)} \sum_{x:x_i=a} |m_i^+(x)\rangle\langle m_i^+(x)|\otimes Q_n(x).

For square matrices define

F_{\mathrm r}(K,L) = \operatorname{Re}\operatorname{tr} \sqrt{\sqrt K\,L\,\sqrt K}, \qquad S(K)=-\operatorname{Re}\operatorname{tr}\bigl[(x\mapsto x\log_2x)(K)\bigr],

where the matrix functions use the real continuous functional calculus. Let $\mathcal P_n=\{i<N:F_{\mathrm r}(P_{n,i}(0),P_{n,i}(1))<2^{-N^\beta}\}$ . With $Q_a=Q_0((a))$ , the asserted limit is

\lim_{n\to\infty}\frac{|\mathcal P_n|}{2^n} = S\!\left(\frac{Q_0+Q_1}{2}\right) -\frac{S(Q_0)+S(Q_1)}2.

The isometry hypothesis cannot hold if $b=0$ or $e=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