Exact polar transform with O(N log N) CNOT/SWAP gates

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.polarTransform_circuit_complexity

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

prove2quantum

For $N=2^n$ , let $G_N=B_NF_2^{\otimes n}$ over $\mathbb F_2$ , acting on row bit vectors. There is a family $C_n$ of circuits consisting of CNOT and SWAP gates, together with an absolute constant $C>0$ and an integer $n_0$ , such that

C_n|u\rangle=|uG_N\rangle\quad\text{for every }n,u,\qquad \operatorname{size}(C_n)\le C\,2^n n\quad(n\ge n_0).

The action is extended linearly to superpositions, and circuit size is the actual gate-list length. At $n=0$ , the one-wire circuit is empty. The bound counts the polar transform; complete encoder phase preparation is a separate node.

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.3,7: the transform has an exact CNOT/SWAP implementation and O(N log N)
elementary gates. One absolute constant and one eventual threshold precede n.
At n=0, N=1 and the circuit is empty. This counts no phase-preparation gates. -/
theorem polarTransform_circuit_complexity :
    ∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ,
      ∃ circuits : (n : ℕ) → List (PolarGate (2 ^ n)),
        circuits 0 = [] ∧
        (∀ n, circuitOperator (circuits n) = polarOperator n) ∧
        (∀ n, n0 ≤ n → ((circuits n).length : ℝ) ≤ C * ((2 : ℝ) ^ n) * (n : ℝ)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 3, §II/IV, unnumbered complexity of the polar transform

Read-back

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

There exist a real constant $C>0$ , a natural number $n_0$ , and, for every natural number $n$ , a finite gate list $L_n$ on $2^n$ Boolean wires, such that $L_0$ is empty, the matrix with entry $1$ precisely at $(v,u)$ satisfying $v=L_n(u)$ equals the matrix with entry $1$ precisely when $v=T_n(u)$ , and

\operatorname{length}(L_n)\le C\,2^n n\qquad(n\ge n_0).

Each gate is either a controlled-NOT with distinct control and target, updating the target by XOR, or a swap of two wires; lists act in their listed order. The transformation $T_n$ has output bit $k$ equal to the parity of those input bits $u_j=1$ for which every $1$ -digit at position $t$ of the $n$ -bit binary expansion of $k$ corresponds to a $1$ -digit at position $n-1-t$ of $j$ , with position $0$ most significant. Matrix equality is required for every $n$ , including $0$ ; only the length bound is restricted to $n\ge n_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