Exact split recursion with the classical flag and history maps

Open

QAlgorithms.Papers.Independent.Intakethird100.P14.split_channel_recursion

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

prove2quantum

Let $W$ be a binary-input classical–quantum channel, let $N=2^n$ , $n\ge0$ , and $1\le i\le N$ . Put $V=W_N^{(i)}$ . Its bad transform averages the second bit, and its good transform retains the first bit as a classical output:

V^-(b)=\frac12\sum_c V(b\oplus c)\otimes V(c),\qquad V^+(c)=\frac12\sum_b |b\rangle\langle b|\otimes V(b\oplus c)\otimes V(c).

For histories $s,t$ of length $i-1$ , relabel the two old history registers by interleaving $s\oplus t$ and $t$ . Keep the physical outputs in their first- $N$ , last- $N$ order. In the good case, append the newly exposed odd bit to the interleaved history. Write $\mathcal R_-$ and $\mathcal R_+$ for these concrete basis relabelings. Both exact identities hold:

W_{2N}^{(2i-1)}=\mathcal R_-(V^-),\qquad W_{2N}^{(2i)}=\mathcal R_+(V^+).

This is the recursion asserted in (16), with registers restored using (6)–(8) and (14)–(15). Printed (18) omits the sum and classical flag; the formal statement records the corrected channel identity rather than that ill-typed expression.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P14

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P14

open Filter MeasureTheory

open scoped ENNReal NNReal ComplexOrder BigOperators

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity)

open QAlgorithms.Papers.Independent.Dependency50.P13 (compression)

open QAlgorithms.Papers.Independent.Renew46.P44 (wordOutput)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- Proposition 7, PDF p.7, corrected (17)–(18). Printed (18) omits the
uniform sum and new odd-bit classical flag, leaving an unbound bit. Changed:
use exactly (14)–(16), pulling back by the concrete history/output maps above.
Why: already N=i=1 the printed spaces disagree; definitions (6)–(8) uniquely
fix this correction. Both exact recursive identities are included. Independent
moderation of this source correction remains required. -/
theorem split_channel_recursion {I : Type} (W : Bit → OutputCoefficients I) (hW : IsBinaryCqChannel W)
    (n : ℕ) (i : PolarWire n) :
    (∀ b (p q : SplitLabel I (n + 1) (childIndex i false)),
      splitChannel W (n + 1) (childIndex i false) b p q =
        channelMinus (splitChannel W n i) b (parentLabels i false p) (parentLabels i false q)) ∧
    (∀ b (p q : SplitLabel I (n + 1) (childIndex i true)),
      splitChannel W (n + 1) (childIndex i true) b p q =
        channelPlus (splitChannel W n i) b (plusLabel i p) (plusLabel i q)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P14

end

Source

Polar codes for classical-quantum channels, arXiv:1109.2591v3, PDF p. 7, Proposition 7: exact split-channel recursion, with the missing classical register restored

Read-back

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

Let $I$ be any type and let $W_b$ , $b\in\mathbb F_2$ , be complex arrays on $I\times I$ , each having an expansion $W_b(a,c)=\sum_r u_r(a)\overline{v_r(c)}$ with $u_r,v_r\in\ell^2(I;\mathbb C)$ and $\sum_r\|u_r\|\|v_r\|<\infty$ , real nonnegative quadratic forms on every finite subset, and summable real diagonal of sum $1$ . For $n\in\mathbb N$ , put $N=2^n$ , define $G_n(r,c)=\prod_{k<n}\kappa(\operatorname{bit}_k(\operatorname{rev}_n r),\operatorname{bit}_k(c))$ , where $\operatorname{rev}_n$ reverses $n$ bits and $\kappa(a,0)=1,\ \kappa(a,1)=a$ , and define $V_u(y,z)=\prod_{c<N}W_{\sum_r u_rG_n(r,c)}(y_c,z_c)$ using arithmetic in $\mathbb F_2$ . For $i<N$ , let $T_{n,i,h,b}=2^{-N}\sum_{v\in\mathbb F_2^N}V_{\operatorname{fill}(h,b,v)}$ , where $\operatorname{fill}(h,b,v)$ agrees with $h\in\mathbb F_2^i$ before $i$ , equals $b$ at $i$ , and agrees with $v$ afterward. Define the binary array $W_{n,i}$ on labels $\mathbb F_2^i\times I^N$ by $W_{n,i}^b((h,y),(h',z))=\mathbf1_{h=h'}2^{-i}T_{n,i,h,b}(y,z)$ . For any binary array $V$ on a label type $L$ , define

V_b^-((a_1,a_2),(c_1,c_2)) =\frac12\sum_{d\in\mathbb F_2}V_{b+d}(a_1,c_1)V_d(a_2,c_2),

and $V_d^+((b,(a_1,a_2)),(b',(c_1,c_2)))=\mathbf1_{b=b'}\tfrac12V_{b+d}(a_1,c_1)V_d(a_2,c_2)$ . Fix any $n\ge0$ and $i<N$ . For a child label $p=(H,y)$ at index $2i$ or $2i+1$ , define

L_-(p)=\bigl((H_{2k}+H_{2k+1})_{k<i},(y_j)_{j<N}\bigr),\qquad L_+(p)=\bigl((H_{2k+1})_{k<i},(y_{N+j})_{j<N}\bigr),

and $L(p)=(L_-(p),L_+(p))$ ; for the child $2i+1$ , also define $L^{+}(p)=(H_{2i},L(p))$ . Then, for every input bit $b$ and every pair of labels $p,q$ of the indicated child, $W_{n+1,2i}^b(p,q)=(W_{n,i})_b^-(L(p),L(q))$ , and $W_{n+1,2i+1}^b(p,q)=(W_{n,i})_b^+(L^{+}(p),L^{+}(q))$ . Both identities include $n=0$ , with empty parent histories.

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