Exact scalable QFT assembly

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.scalable_qft

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

prove2quantum

Let $m,k\ge2$ be integers. Let $C_{m,k}$ be the chronological circuit obtained by starting with $QFT_m$ and, for each $t=1,\ldots,k-1$ , applying adjacent two-block phase-swaps of types $t,t-1,\ldots,1$ at offsets $(t-1)m,(t-2)m,\ldots,0$ , then $QFT_m$ at offset zero. A type- $j$ phase-swap maps $|a,b\rangle$ to $e^{2\pi iab/2^{(j+1)m}}|b,a\rangle$ , with both integers read most significant bit first. The Fourier transform has positive exponential sign and normalization $2^{-km/2}$ . Then

C_{m,k}=QFT_{km},\qquad \#QFT_m=k,\qquad\#CP=\binom{k}{2},\qquad\#CP_j=k-j\quad(1\le j<k).

There are no other phase-swap types. This is an exact assembly identity, including the complete final permutation and phase; it makes no physical timing claim.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF pp.1,9, abstract headline pinned to Fig.7: the exact scalable QFT
assembly and its actual block counts. No timing or global optimization claim. -/
theorem scalable_qft (m k : ℕ) (hm : 2 ≤ m) (hk : 2 ≤ k) :
    blockCircuitMatrix (k * m) (qftAssembly m k) = qftQubits (k * m) ∧
    fourierCount (qftAssembly m k) = k ∧
    phaseTotal (qftAssembly m k) = Nat.choose k 2 ∧
    (∀ j, 1 ≤ j → j < k → phaseCount j (qftAssembly m k) = k - j) ∧
    (∀ j, j = 0 ∨ k ≤ j → phaseCount j (qftAssembly m k) = 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P39

Source

Quantum CISC Compilation by Optimal Control and Scalable Assembly of Complex Instruction Sets beyond Two-Qubit Gates, arXiv:0712.3227v2, PDF p. 9, Abstract headline pinned to exact scalable QFT assembly, Fig. 7

Read-back

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

For all natural numbers $m,k$ satisfying $m\ge2$ and $k\ge2$ , form a list $C$ by concatenating, for $t=0,\ldots,k-1$ in increasing order, phase-swap records $(sm,m,s+1)$ for $s=t-1,\ldots,0$ in decreasing order, followed by a Fourier record $(0,m)$ ; a phase-swap record lists its offset, half-width, and phase index, and a Fourier record lists its offset and width. For a bit string $x$ of length $r$ , let $v(x)=\sum_{a=0}^{r-1}x_a2^{r-1-a}$ , with bits interpreted as $0$ or $1$ . On a local width- $m$ block, the Fourier matrix has entry $\exp(2\pi\mathrm{i}\,v(y)v(x)/2^m)/\sqrt{2^m}$ . A phase-swap record with half-width $m$ and phase index $p$ has, for input halves $(a,b)$ , its only nonzero entry at output $(b,a)$ , equal to $\exp(2\pi\mathrm{i}\,v(a)v(b)/2^{(p+1)m})$ . Each local matrix acts at its stated offset and leaves the other bits unchanged. The theorem asserts the conjunction of the following facts: the reverse-ordered product of the matrices of $C$ , acting on $km$ bits, has entries

U_{y,x}=\frac{\exp(2\pi\mathrm{i}\,v(y)v(x)/2^{km})}{\sqrt{2^{km}}};

the list contains exactly $k$ Fourier records and exactly $\binom{k}{2}$ phase-swap records; for every natural number $j$ with $1\le j<k$ , exactly $k-j$ phase-swap records have phase index $j$ ; and for every natural number $j$ satisfying $j=0$ or $k\le j$ , no phase-swap record has phase index $j$ . Here $k-j$ is natural-number subtraction, and its stated range ensures no truncation.

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