TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Quantum counting query complexity

Statement

For an integer $n \geq 0$ , $N = 2^{n}$ , and a power of two $M = 2^{m} \geq 4$ , Count uses exactly $M - 1$ repeated controlled-Grover calls, or exactly $m$ supplied controlled-power queries, in addition to its $n$ ordinary Hadamards for uniform-state preparation. At fixed success probability, additive count error $ϵ_{c} \in (0, N]$ is obtained using $O (N / ϵ_{c})$ repeated controlled-Grover calls; additive fraction error $ϵ_{f} \in (0, 1]$ uses $O (1 / ϵ_{f})$ . The count-dependent error bound retains the terms $2 π k \sqrt{t (N - t)} / M$ and $π^{2} k^{2} N / M^{2}$ . Algebraic output encoding and integer rounding have separate classical bit costs.

Facts & Assumptions

Given: The counting algorithm, an integer $n \geq 0$ , $N = 2^{n}$ , a power-of-two $M \geq 4$ , and the declared query mode.

[F1]

The estimator has the phase-estimation circuit and uniform preparation specified in Quantum counting by uniform-state amplitude estimation.

[F2]

Repeated controlled- $Q$ access costs $M - 1$ calls and supplied powers cost $m$ calls (Amplitude-estimation query and precision complexity).

[F3]

The additive amplitude guarantee is the statement of Amplitude-estimation additive error and success probability.

[F4]

Query counts and classical bit operations are separate resources (Quantum query complexity, Classical bit-operation cost).

Proof

1.1givenF1F2F4

The exact controlled-iterate counts follow from [F2]. The uniform address preparation applies one Hadamard to each of the $n$ wires by [F1], in addition to phase-register and QFT gates separately counted in [F4].

2.1givenF3step 1.1algebra

For fraction error $ϵ_{f}$ , set amplitude precision $ϵ = ϵ_{f}$ ; for count error $ϵ_{c}$ , set $ϵ = ϵ_{c} / N$ . Choosing $M$ the least power of two at least $4 (22 / 7) / ϵ$ makes the $k = 1$ error $π / M + π^{2} / M^{2} < ϵ$ for $ϵ \leq 1$ by [F3]. The least-power bound is $M < 8 (22 / 7) / ϵ$ , giving the two asymptotic query bounds.

3.1givenF3F4step 2.1algebra∎

The count-dependent expression is [F3] multiplied by $N$ as in Quantum counting error and boundary cases. Multiplication by $N$ , exact cyclotomic representation, and optional integer rounding are classical bit work and remain separate under [F4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

Brassard, Høyer, Mosca, and Tapp, Quantum Amplitude Amplification and Estimation, complete article, §§4–5, Theorems 11–18 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms, complete lecture notes, §§19.1–19.3 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, complete 239-page notes, §7.3 (standard reference, not scraped)