TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Truncated QFT ideal gate count

Statement

For $n \geq 1$ and integer $m \geq 1$ , put $\tilde{m} = \min {m, n}$ . The truncated binary QFT uses $n$ Hadamards, $\sum_{s = 2}^{\tilde{m}} (n - s + 1)$ controlled phases, $⌊ n / 2 ⌋$ SWAP gates and no ancillas. Its ideal gate count is therefore

$n + \sum_{s = 2}^{\tilde{m}} (n - s + 1) + ⌊ n / 2 ⌋ = O (n \tilde{m} + n) .$

For fixed $c > 0$ , if $n \geq 2$ , $n^{- c} \leq ε < 1$ , and $m = \min {n, ⌈ \log_{2} (2 π n / ε) ⌉}$ , then $\tilde{m} = O_{c} (\log n)$ and this count is $O_{c} (n \log n)$ ideal gates. Expanding the reversal replaces each SWAP by three exact CNOTs; no finite-set synthesis count is asserted here.

Facts & Assumptions

Given: The truncated circuit with $n \geq 1$ and integer cutoff $m \geq 1$ .

[F1]

The truncated circuit retains every Hadamard, every controlled phase with $2 \leq s \leq m$ , every final reversal SWAP, and no ancillas (Truncated binary QFT).

[F2]

Each retained Hadamard, controlled phase and SWAP has ideal cost one; a SWAP may instead be expanded to three exact CNOTs (QFT ideal and finite-set gate-cost models).

[F3]

Each two-wire SWAP equals the exact three-CNOT sequence (A SWAP Is Three CNOTs).

[F4]

For $0 < ε < 1$ , choosing $m = \min {n, ⌈ \log_{2} (2 π n / ε) ⌉}$ gives the stated truncation error at most $ε$ (Operator-norm error of QFT truncation).

Proof

technique · direct

Given: The circuit and counting convention above.

1.1F1algebra

For each target $q_{j}$ , the exact circuit has $j$ controlled phases. A retained denominator level $s$ corresponds to pairs with $j - i + 1 = s$ , namely $i = 0, \dots, n - s$ , and so has $n - s + 1$ gates. The cutoff retains precisely $s = 2, \dots, \tilde{m}$ . If $m \geq n$ , then $\tilde{m} = n$ and every phase is retained.

2.1F1F2F3F4step 1.1algebra∎

There are $n$ target wires, $⌊ n / 2 ⌋$ final swaps, and no other gates or ancillas by [F1]. Summing their costs by [F2] gives the formula. Since $\sum_{s = 2}^{\tilde{m}} (n - s + 1) \leq n (\tilde{m} - 1)$ and $⌊ n / 2 ⌋ \leq n / 2$ , the total is at most $n \tilde{m} + n / 2$ , hence $O (n \tilde{m} + n)$ . Under the cutoff in [F4] and $ε \geq n^{- c}$ , $m \leq ⌈ \log_{2} (2 π n^{c + 1}) ⌉ = O_{c} (\log n)$ , so $\tilde{m} = O_{c} (\log n)$ . The CNOT expansion is exact by [F3] and changes only the final reversal term; it does not compile any rotation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ronald de Wolf, Quantum Computing: Lecture Notes (arXiv:1907.09415v6) (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (standard reference, not scraped)