Classical polar encoding uses O(N log N) actual XOR and swap gates

Open

QAlgorithms.Papers.Independent.Intakethird100.P14.classical_encoding_complexity

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

prove2quantum

For each $N=2^n$ , let $G_N=B_NF^{\otimes n}$ over $\mathbb F_2$ , where $F=\left[\begin{smallmatrix}1&0\\1&1\end{smallmatrix}\right]$ and $B_N$ reverses the $n$ address bits of a wire. Form the explicit classical circuit $E_n$ by swapping each bit-reversal wire pair once and then applying the $n$ XOR butterfly layers. Count every two-wire XOR and swap as one operation. There exist absolute constants $C>0$ and $n_0\in\mathbb N$ such that the cost bound holds for every $n\ge n_0$ , and correctness holds for every $n\ge0$ :

|E_n|\le C\,2^n n,\qquad \forall u\in\mathbb F_2^{2^n},\quad E_n(u)=uG_{2^n}.

Since $n=\log_2N$ , the actual list length is $O(N\log N)$ . The circuit and bound are independent of the transmitted word, information set, and frozen vector. The claim concerns classical encoding; no efficient quantum decoding theorem is supplied by the paper.

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

/-- Unnumbered main contribution, PDF pp.1–2; actual encoder (5), p.4.
The concrete XOR/swap list implements uG_N on every word. Universal constants
and the threshold precede n and the input, hence also all coset choices.
Since N=2^n, N*n is exactly N*log_2(N). No quantum decoding complexity is claimed. -/
theorem classical_encoding_complexity :
    ∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ,
      (∀ n ≥ n0, ((recursivePolarEncoder n).length : ℝ) ≤ C * (2 ^ n : ℕ) * n) ∧
      ∀ n (u : PolarWire n → Bit), runEncoder (recursivePolarEncoder n) u = polarEncode n u := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P14

end

Source

Polar codes for classical-quantum channels, arXiv:1109.2591v3, PDF p. 2, Unnumbered main result: O(N log N) classical polar encoding

Read-back

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

There exist a real constant $C>0$ and an integer $n_0\ge0$ such that the following gate-count bound holds for every $n\ge n_0$ , and the following encoding identity holds for every $n\ge0$ and every word $u:\{0,\ldots,2^n-1\}\to\mathbb F_2$ . Write $\operatorname{rev}_n(i)$ for the index obtained by reversing the $n$ binary digits of $i$ , reduced modulo $2^n$ , and write $\operatorname{toggle}_k(i)=(i\mathbin{\mathrm{xor}}2^k)\bmod2^n$ . The prescribed gate list first swaps $i$ with $\operatorname{rev}_n(i)$ for every $i<\operatorname{rev}_n(i)$ , in the order supplied by the finite set’s list, and then, for $k=0,\ldots,n-1$ in increasing order, applies an XOR gate from $\operatorname{toggle}_k(i)$ to $i$ for each $i$ whose $k$ -th binary digit is $0$ , again in the finite set’s list order. An XOR gate replaces its target value by the sum modulo $2$ of the old target and source values; a swap exchanges the two old values. The length $L_n$ of this list satisfies

L_n\le C\,2^n n\qquad(n\ge n_0).

Executing the entire list in order gives, at each output coordinate $c<2^n$ , exactly

\sum_{r<2^n}u_r \prod_{k<n}\kappa\!\left( \operatorname{bit}_k(\operatorname{rev}_n(r)),\operatorname{bit}_k(c)\right), \qquad \kappa(a,0)=1,\quad\kappa(a,1)=a,

where all sums and products are in $\mathbb F_2$ . The identity is not restricted to $n\ge n_0$ . In particular, $n=0$ has one wire, an empty gate list, and an empty product equal to $1$ .

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