Exact QFT assembly with half-block phase-swaps

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.scalable_qft_variantII

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

prove2quantum

Let $m\ge2$ be even and let $k\ge2$ . In the Fig. 7 circuit replace each phase-swap of type $j$ and half-width $m=2h$ , at offset $a$ , by the chronological four-module list

CP_{2j}(a+h),\quad CP_{2j-1}(a),\quad CP_{2j+1}(a+2h),\quad CP_{2j}(a+h),

where each new module has half-width $h$ and total width $m$ . The resulting explicit Fig. 16 circuit satisfies

C^{\rm II}_{m,k}=QFT_{km},\qquad\#QFT_m=k,\qquad\#CP=4\binom{k}{2}.

Only phase indices $1,\ldots,2k-1$ occur. This preserves every phase and permutation. Three bottom label occurrences printed $2m$ (two phase types) in Fig. 16 are interpreted as $m$ , following the caption and half-block construction; this minimal arity correction was independently checked in moderation round 1.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF p.19, Fig.16: exact QFT variant II. The three printed bottom arity
labels 2m (two phase types) are read as m, as required by the caption and half-block widths;
this correction is recorded for independent moderation. -/
theorem scalable_qft_variantII (m k : ℕ) (hm : 2 ≤ m) (heven : Even m) (hk : 2 ≤ k) :
    blockCircuitMatrix (k * m) (qftAssemblyII m k) = qftQubits (k * m) ∧
    fourierCount (qftAssemblyII m k) = k ∧
    phaseTotal (qftAssemblyII m k) = 4 * Nat.choose k 2 ∧
    (∀ j, j = 0 ∨ 2 * k ≤ j → phaseCount j (qftAssemblyII 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. 19, Appendix A, Fig. 16: QFT variant II

Read-back

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

For all natural numbers $m,k$ satisfying $m\ge2$ , $m$ even, and $k\ge2$ , put $h=m/2$ and form a list $C$ as follows: for $t=0,\ldots,k-1$ in increasing order, and within each $t$ for $s=t-1,\ldots,0$ in decreasing order, append the four phase-swap records

(sm+h,h,2s+2),\quad (sm,h,2s+1),\quad (sm+2h,h,2s+3),\quad (sm+h,h,2s+2),

then append a Fourier record with offset $0$ and width $m$ . A phase-swap triple specifies offset, half-width, and phase index. For a length- $r$ bit string $x$ , let $v(x)=\sum_{a=0}^{r-1}x_a2^{r-1-a}$ , interpreting bits as $0$ or $1$ . The local Fourier matrix has entries $\exp(2\pi\mathrm{i}\,v(y)v(x)/2^m)/\sqrt{2^m}$ . A local phase-swap matrix of half-width $h$ and phase index $p$ has its only nonzero entry for input $(a,b)$ at output $(b,a)$ , equal to $\exp(2\pi\mathrm{i}\,v(a)v(b)/2^{(p+1)h})$ . Each matrix is placed at the record’s offset, leaving the other bits unchanged. The theorem asserts that the reverse-ordered product of these matrices on $km$ bits has entries

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

that $C$ contains exactly $k$ Fourier records and exactly $4\binom{k}{2}$ phase-swap records, and that, for every natural number $j$ satisfying $j=0$ or $2k\le j$ , the number of phase-swap records in $C$ with phase index $j$ is zero.

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