TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Phase-estimation query and gate costs

Statement

Let $m \geq 1$ and $Q = 2^{m}$ . Count costs in the ideal continuous-rotation submodel, where each exact controlled phase used by the binary QFT is one gate. If the controlled powers $C (U^{2^{j}})$ , $0 \leq j < m$ , are supplied as one query each, one run uses exactly $m$ controlled-power queries. If the only oracle is $C (U)$ , the repeated implementation uses exactly $Q - 1$ controlled- $U$ queries. If the supplied controlled-power circuits have ordinary gate counts $C_{j}$ , the unitary gate count after the eigenstate input is provided is $\sum_{j = 0}^{m - 1} C_{j} + 2 m + \frac{m (m - 1)}{2} + ⌊ \frac{m}{2} ⌋ .$ The final register measurement reads $m$ bits and is not included in this unitary gate count. No cost-free power construction, fixed finite gate alphabet, uniform family, or state-preparation bound is asserted.

Facts & Assumptions

Given: The $m$ -bit QPE procedure, $Q = 2^{m}$ , and the ideal gate-cost convention stated above.

[F1]

The QPE procedure applies one controlled $U^{2^{j}}$ for each $j = 0, \dots, m - 1$ , with $m$ Hadamards to prepare the phase register (Quantum phase estimation).

[F2]

Under single-controlled-unitary access, one call is the control-first block $C (U) = diag (I_{H}, U)$ ; the eigenphase-estimation model permits the $j$ th controlled power to be implemented by $2^{j}$ sequential calls (Controlled Unitary Access, Eigenphase estimation access model).

[F3]

The exact $m$ -wire QFT circuit uses $m$ Hadamards, $m (m - 1) / 2$ controlled phases, and $⌊ m / 2 ⌋$ named swaps in the ideal model; its inverse has the same count (Exact binary QFT ideal gate count).

[F5]

The operation model may assign gate, classical-bit, and query costs separately, and each coordinate counts the calls actually made (Finite circuit resource accounting).

[F4]

The natural-valued sum $S_{n} : = \sum_{j < n} 2^{j}$ has $S_{0} = 0$ and $S_{n + 1} = S_{n} + 2^{n}$ (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[F6]

Natural powers satisfy $2^{0} = 1$ and $2^{n + 1} = 2^{n} \cdot 2$ ; natural multiplication satisfies $a \cdot 2 = a + a$ , using $a \cdot 1 = a$ (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ , Multiplication of natural numbers, Zero and one under multiplication).

[F7]

Natural induction is valid, and natural addition is associative and commutative (The principle of mathematical induction, Addition is associative, Addition is commutative).

Proof

1.1F1givenalgebra

Under controlled-power access, the loop in [F1] invokes exactly one supplied operation for each of the $m$ indices $j = 0, \dots, m - 1$ , hence exactly $m$ controlled-power queries.

1.2F2F4F6F7givenbaseihdischarge-induction

Under single controlled-unitary access, the repeated implementation specified by the procedure uses $2^{j}$ sequential calls to $C (U)$ for the controlled power at index $j$ [F2], so the total query count is the natural sum $S_{m}$ . To identify this natural-valued sum, prove $S_{n} + 1 = 2^{n}$ by induction. At $n = 0$ , $S_{0} + 1 = 0 + 1 = 1 = 2^{0}$ . If $S_{n} + 1 = 2^{n}$ , then [F4, F6, F7] give $S_{n + 1} + 1 = (S_{n} + 2^{n}) + 1 = (S_{n} + 1) + 2^{n} = 2^{n} + 2^{n} = 2^{n} \cdot 2 = 2^{n + 1}$ . Hence $S_{m} + 1 = 2^{m} = Q$ ; by the defining truncated difference in [F4]'s source and commutativity of addition, $S_{m} = Q - 1$ .

1.3F1F3givenalgebra

The supplied power circuits contribute $\sum_{j} C_{j}$ ordinary gates. Phase-register preparation contributes $m$ Hadamards, and the inverse QFT contributes the count in [F3]. Adding gives the displayed unitary gate count; reversing the QFT circuit changes neither its count nor the query count.

2.1F5step 1.1step 1.2step 1.3∎

Measurement outputs one $m$ -bit label. The operation model [F5] keeps query, ordinary-gate, and classical-bit costs separate; the input eigenstate's preparation is outside the theorem's stated count. Therefore the displayed formula asserts only the stated gate profile and does not infer an implementation of powers from a black-box $U$ .

Depends on

Used by

Bounded-error evaluation from a dual adversary certificate Algorithm
QFT-based amplitude estimation Algorithm
Szegedy-walk marked-set detection Algorithm
Amplitude-estimation additive error and success probability Theorem
Amplitude-estimation query and precision complexity Theorem
Dual reflection evaluator has bounded-error correctness Theorem
Dual reflection evaluator query complexity Theorem
Element-distinctness gate cost in the QRAM model Theorem
Finite reversible-walk finding cost Theorem
Relative approximate counting query complexity Theorem
Separate order-finding query, gate, and bit costs Theorem
Walk detection correctness and cost Theorem

Dependency tree · two levels

57 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

Andrew M. Childs, Lecture Notes on Quantum Algorithms, §4.3 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, version 6, §4.6 (standard reference, not scraped)