ExampleConstruction: Literature-sourcedVerification: 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.

QFT circuit order and truncation examples

Example

For $N = 4$ ( $n = 2$ ), the positive-sign exact circuit in standard wire order $q_{1}, q_{0}$ is $H (q_{1})$ , then ${C P}_{2} (q_{0}, q_{1})$ , then $H (q_{0})$ , then $S W A P (q_{1}, q_{0})$ . Its matrix in basis order $∣ 00 ⟩, ∣ 01 ⟩, ∣ 10 ⟩, ∣ 11 ⟩$ is

$F_{4}^{+} = \frac{1}{2} (\begin{array}{cccc} 1 & 1 & 1 & 1 \\ 1 & i & - 1 & - i \\ 1 & - 1 & 1 & - 1 \\ 1 & - i & - 1 & i \end{array}) .$

If the same register is displayed in reversed wire order $q_{0}, q_{1}$ , the matrix in that order is $P F_{4}^{+} P$ , where $P$ swaps the middle two basis vectors:

$P F_{4}^{+} P = \frac{1}{2} (\begin{array}{cccc} 1 & 1 & 1 & 1 \\ 1 & 1 & - 1 & - 1 \\ 1 & - 1 & i & - i \\ 1 & - 1 & - i & i \end{array}) .$

With cutoff $m = 1$ , the only controlled phase ${C P}_{2}$ is omitted, while the two Hadamards and final swap remain. The exact circuit has $2$ Hadamards, one controlled phase and one SWAP ( $4$ ideal gates, or $6$ gates after expanding the SWAP); the truncated circuit has $2$ Hadamards and one SWAP ( $3$ ideal gates, or $5$ with that expansion). Its operator-norm difference from the exact circuit is $\sqrt{2}$ , and the general omitted-gate sum is $π / 2$ for this $n, m$ .

Facts & Assumptions

Given: Two ordered qubits, the Hadamard and controlled-phase matrices below, the positive-sign $N = 4$ Fourier matrix, and the wire-swap permutation.

[L1]

The gate matrices are $H = 2^{- 1 / 2} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array})$ and ${C P}_{2} = diag (1, 1, 1, i)$ from QFT ideal and finite-set gate-cost models.

[L2]

The exact chronological gate list and the cutoff- $1$ deletion are those in Exact binary QFT circuit and Truncated binary QFT.

[L3]

The positive-sign QFT formula at $N = 4$ gives basis amplitudes $(F_{4}^{+})_{y, x} = \frac{1}{2} e^{π i x y / 2}$ in binary basis order $00, 01, 10, 11$ (Positive-sign cyclic quantum Fourier transform).

[L4]

$P$ is the permutation matrix exchanging $∣ 01 ⟩$ and $∣ 10 ⟩$ and fixing $∣ 00 ⟩, ∣ 11 ⟩$ .

[F1]

The A-page lemma proves $\sqrt{2} < π / 2$ from the cosine series (The half-turn constant exceeds $\sqrt{2}$ ).

[F2]

A SWAP on two ordered qubits equals the exact three-CNOT circuit (A SWAP Is Three CNOTs).

[F3]

The ideal QFT gate-count model assigns one count to each Hadamard, controlled phase and named SWAP (QFT ideal and finite-set gate-cost models).

[F4]

A gate on specified wires has a unitary global embedding that acts by the local gate there and by identity elsewhere (A local gate has a unique global wire embedding).

[F5]

A finite-dimensional unitary preserves norms and has inverse its adjoint (For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and $T^{*} T = I$ are equivalent).

[F6]

Euler's formula gives $e^{i θ} = \cos θ + i \sin θ$ for real $θ$ (Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ ).

[F7]

The quarter-turn values include $\sin (π / 2) = 1$ , $\cos (π / 2) = 0$ , $\sin π = 0$ , $\cos π = - 1$ , with the shift identities used at $3 π / 2$ (Quarter-turn values and shifts by pi/2 and pi).

[F8]

On a nonzero finite-dimensional domain, the operator norm is the maximum over unit vectors (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

[F9]

Complex modulus satisfies $z \overline{z} = ∣ z ∣^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F10]

The ordered product basis of the two-qubit register is orthonormal (The product basis is orthonormal and tensor dimensions multiply).

[F11]

For cutoff $m = 1$ , the operator-norm estimate sums $(n - s + 1) 2 π / 2^{s}$ over $s = 2, \dots, n$ (Operator-norm error of QFT truncation).

[F12]

The complex exponential satisfies $\exp (z + w) = \exp z \exp w$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[L5]

Kets denote vectors, and the standard-basis kets are coordinate vectors (Dirac Notation Conversion).

[A1]

Denotational semantics of a finite layered circuit identifies the chronological gate list with the right-to-left product of its embedded gate operators.

Verification

technique · direct finite calculation

Given: The two-qubit gate lists and conventions in [L1]–[L4].

1.1L1L2L3L5F4F6F7F12A1algebra

On basis input $∣ x_{1} x_{0} ⟩$ , after $H (q_{1})$ and ${C P}_{2} (q_{0}, q_{1})$ the $q_{1}$ factor is $2^{- 1 / 2} (∣ 0 ⟩ + (- 1)^{x_{1}} i^{x_{0}} ∣ 1 ⟩)$ ; after $H (q_{0})$ the $q_{0}$ factor is $2^{- 1 / 2} (∣ 0 ⟩ + (- 1)^{x_{0}} ∣ 1 ⟩)$ . The local gate actions are [F4], and their composition in chronological order requires [A1]. Euler's formula and the quarter-turn values [F6,F7] give $e^{i π / 2} = i$ , $e^{i π} = - 1$ , and $e^{3 π i / 2} = - i$ . For the nonnegative integer $x y$ , iterating [F12] gives $e^{π i x y / 2} = (e^{i π / 2})^{x y} = i^{x y}$ , with both sides $1$ when $x y = 0$ . After the final swap the factors are ordered as the $q_{0}$ factor followed by the $q_{1}$ factor. Substituting $x_{1} x_{0} = 00, 01, 10, 11$ gives the four columns $[1, 1, 1, 1]^{T}$ , $[1, i, - 1, - i]^{T}$ , $[1, - 1, 1, - 1]^{T}$ , and $[1, - i, - 1, i]^{T}$ , each divided by $2$ ; these are the amplitudes in [L3].

1.2L1L2L5F1F4F5F8F9F10F11A1algebra

By [L2,A1], the difference of exact and cutoff operators is $S H (q_{0}) ({C P}_{2} - I) H (q_{1})$ , where the left and right factors are unitary: $H^{*} H = I$ , ${C P}_{2}$ is diagonal with unit-modulus entries, and $S$ permutes an orthonormal basis [L1,F5,F9,F10]. Thus left multiplication preserves norms and right multiplication maps the unit sphere onto itself, so the difference has operator norm $∥ {C P}_{2} - I ∥$ by [F5,F8]. Write a unit vector as $v = \sum_{a, b \in {0, 1}} c_{a b} ∣ a b ⟩$ . By [F10], $\sum_{a, b} ∣ c_{a b} ∣^{2} = 1$ . The operator ${C P}_{2} - I$ sends $v$ to $(i - 1) c_{11} ∣ 11 ⟩$ , and [F9] gives $∣ i - 1 ∣^{2} = (i - 1) (- i - 1) = 2$ . Hence $∥ ({C P}_{2} - I) v ∥^{2} = 2 ∣ c_{11} ∣^{2} \leq 2$ , with equality at $v = ∣ 11 ⟩$ ; [F8] gives $∥ {C P}_{2} - I ∥ = \sqrt{2}$ . The bound in [F11] is $(2 - 2 + 1) 2 π / 2^{2} = π / 2$ for $n = 2, m = 1$ , and [F1] gives $\sqrt{2} < π / 2$ .

2.1L3L4L5A1step 1.1algebra

Reversing the displayed wire order permutes both the input and output basis by $P$ , so the matrix is $P F_{4}^{+} P$ by the tensor-register convention [L4]. Swapping rows and columns $2$ and $3$ gives $\frac{1}{2} (\begin{array}{cccc} 1 & 1 & 1 & 1 \\ 1 & 1 & - 1 & - 1 \\ 1 & - 1 & i & - i \\ 1 & - 1 & - i & i \end{array})$ , which is the displayed reversed-order matrix.

3.1L1L2F2F3algebra∎

The exact list has $2 + 1 + 1 = 4$ ideal gates, and its one SWAP adds three CNOTs by [F2]; the ideal convention is [F3]. The cutoff list has $2 + 1 = 3$ ideal gates and the same three-CNOT expansion. Neither circuit introduces an ancilla.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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