LemmaStatement: 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.

Binary factorization of QFT basis output

Statement

Let $n \geq 0$ , $N = 2^{n}$ , and take the input word $(x_{n - 1}, \dots, x_{0})$ in wire order $q_{n - 1}, \dots, q_{0}$ . By the big-endian index convention, its integer is $x = \sum_{i = 0}^{n - 1} x_{i} 2^{i}$ , with $x_{i} \in {0, 1}$ . For $0 \leq j < n$ , set

$R_{j} : = 2^{- 1 / 2} (∣ 0 ⟩ + e^{2 π i \sum_{i = 0}^{j} x_{i} 2^{- (j - i + 1)}} ∣ 1 ⟩) .$

With the register order $q_{n - 1}, \dots, q_{0}$ , the standard-basis output ${QFT}_{2^{n}} ∣ x ⟩$ is $R_{0} \otimes R_{1} \otimes \dots \otimes R_{n - 1}$ . The ordered factors immediately before the final wire-reversal permutation of the exact circuit are $R_{n - 1} \otimes \dots \otimes R_{0}$ . For $n = 0$ , both are the empty tensor product, interpreted as the scalar $1$ .

Facts & Assumptions

Given: The positive-sign transform ${QFT}_{2^{n}}$ of Positive-sign cyclic quantum Fourier transform, binary input encoding by Big-endian encoding of ordered bit strings, ordered tensor registers and reversal permutation by Ordered tensor registers, their inner product, and wire permutations, the standard ket convention of Dirac Notation Conversion, and bijectivity of the binary index.

[F1]

The map ${enc}_{n}$ is a bijection from length- $n$ bit strings to ${0, \dots, 2^{n} - 1}$ (Big-endian bit-string indices are bijective).

[F2]

A bit tuple $(b_{0}, \dots, b_{n - 1})$ has big-endian index $\sum_{k < n} b_{k} 2^{n - 1 - k}$ , so the first listed wire is most significant (Big-endian encoding of ordered bit strings).

[F3]

The product basis is ordered lexicographically by factor indices, and a wire permutation sends a product-basis tuple to the tuple in the permuted factor order (Ordered tensor registers, their inner product, and wire permutations).

[F4]

A ket denotes its vector, and the standard coordinate kets are the corresponding coordinate vectors (Dirac Notation Conversion).

[L1]

The definition Positive-sign cyclic quantum Fourier transform gives the basis amplitude $2^{- n / 2} e^{2 π i x y / 2^{n}}$ at output integer $y$ .

[F5]

The Hadamard sends $∣ b ⟩$ to $2^{- 1 / 2} (∣ 0 ⟩ + (- 1)^{b} ∣ 1 ⟩)$ for $b \in {0, 1}$ (Exact one-qubit gates and rotations).

[F6]

The controlled phase $C P (θ)$ fixes $∣ 00 ⟩, ∣ 01 ⟩, ∣ 10 ⟩$ and multiplies $∣ 11 ⟩$ by $e^{i θ}$ (Controlled Phase Rotation).

Proof

technique · direct

Given: $n \geq 0$ , an input bit string $x_{0}, \dots, x_{n - 1}$ , and the stated ordered-basis conventions.

1.1givenF1F2L1algebra

For $n \geq 1$ , bijectivity [F1] lets us index the output basis by all bit words $(y_{n - 1}, \dots, y_{0})$ in wire order; [F2] gives $y = \sum_{j = 0}^{n - 1} y_{j} 2^{j}$ . Then $x y / 2^{n} = \sum_{j} y_{j} x / 2^{n - j}$ . In the term indexed by $y_{j}$ , put $k = n - 1 - j$ . The fractional part of $x / 2^{n - j}$ is $\sum_{i = 0}^{k} x_{i} 2^{- (k - i + 1)}$ : terms with $i > k$ are integers and the remaining powers have exactly these denominators. Thus the phase attached to output bit $y_{j}$ is the phase of $R_{n - 1 - j}$ .

2.1givenF3F4L1step 1.1algebra

Consequently $e^{2 π i x y / 2^{n}} = \prod_{j} e^{2 π i y_{j} \sum_{i = 0}^{n - 1 - j} x_{i} 2^{- (n - j - i)}}$ . Summing over all bit strings $y$ factors as a tensor product of the two-term sums for the individual $y_{j}$ ; the normalization $2^{- n / 2}$ is the product of the $n$ factors $2^{- 1 / 2}$ . By [F3], in wire order $q_{n - 1}, \dots, q_{0}$ the factor sequence is $R_{0} \otimes \dots \otimes R_{n - 1}$ , and [F4] identifies these coordinate factors with the corresponding kets.

3.1givenF3F5F6step 2.1algebra∎

In the descending-target circuit, the block on $q_{j}$ applies $H$ followed by $C P (2 π / 2^{j - i + 1})$ from each control $q_{i}$ with $i < j$ . Before this block, all lower wires are still in the basis states $∣ x_{i} ⟩$ : previous blocks target only higher wires, and [F6] leaves basis controls unchanged. By [F5], the Hadamard contributes relative phase $(- 1)^{x_{j}} = e^{2 π i x_{j} / 2}$ ; by [F6], the controlled phases multiply it by $\prod_{i < j} e^{2 π i x_{i} / 2^{j - i + 1}}$ . Thus the block prepares $R_{j}$ without changing the lower wires or previously prepared higher factors. Induction down the finite loop gives $R_{n - 1} \otimes \dots \otimes R_{0}$ before reversal. By [F3], reversal gives the output of step 2.1. At $n = 0$ , the loop is empty, $N = 1$ , and both states are the empty tensor $1$ .

Remarks

The binary fraction in $R_{j}$ is $0. x_{j} x_{j - 1} \dots x_{0}$ in base two. In particular, the output factor order and the pre-swap factor order differ; suppressing the final reversal changes the bit convention.

Depends on

Used by

Exact binary QFT circuit Algorithm
Exact binary QFT circuit correctness Theorem

Dependency tree · two levels

40 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)