TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Grover search upper-bound success guarantee

Statement

On every promised input of All-zero versus exactly-one-marked search promise, the fixed-one procedure Fixed-one Grover search with candidate verification returns the correct decision and, on a one-marked input, its marked coordinate with probability at least $1 - 1 / M$ , where $M = 2^{⌈ \log_{2} N ⌉}$ and $M = 1$ when $N = 1$ . In particular, its one-marked success probability is at least $1 - 1 / N$ ; when $N = 1$ it succeeds with certainty. On $0^{N}$ verification always returns no.

Facts & Assumptions

Given: The fixed-one schedule, its reversible simulation of the padded oracle, the exact recurrence identity, and the integer-rounding theorem.

[F1]

Fixed-one Grover search with candidate verification: the procedure pads to $M$ , fixes its schedule count to $1$ , maximizes $p_{k} = (1 - T_{2 k + 1} (1 - 2 / M)) / 2$ over $0 \leq k \leq ⌈ \sqrt{M} ⌉$ , and verifies the measured candidate by initializing the XOR-query response to $0$ and measuring the resulting bit.

[F2]

Zero-completed query simulation is exact and uses one raw query: each padded query is exactly simulated using one raw query, and padded addresses have value zero.

[F3]

The rational Grover recurrence equals the success probability: for a dyadic domain and exact mark count $t$ , the recurrence value $p_{k}$ equals the actual Grover marked-address probability.

[F4]

Integer rounding gives a high-success Grover iterate: if $0 < t / M \leq 1 / 2$ , some $k \leq ⌈ \sqrt{M / t} ⌉$ has Grover success at least $1 - t / M$ ; for $t / M > 1 / 2$ , $k = 0$ has success $t / M$ .

[F5]

All-zero versus exactly-one-marked search promise: on a one-mark input the padded length- $M$ string has exactly one marked valid address, while the zero input has no marked address.

Proof

1.1F1F3F5algebra

If $N = 1$ , then $M = 1$ and the schedule in [F1] includes $k = 0$ . Its recurrence value is $p_{0} = (1 - (- 1)) / 2 = 1$ , since $1 - 2 / M = - 1$ and $T_{1} (q) = q$ . The maximizing choice in [F1] has value at least $p_{0}$ , and [F3] identifies every list value with a probability at most $1$ , so the selected success probability is $1$ . If $N \geq 2$ , then $M \geq 2$ , so the padded one-mark input in [F5] has ratio $t / M = 1 / M \leq 1 / 2$ .

2.1F1F3F4step 1.1

For $N \geq 2$ , [F4] supplies an integer $k \leq ⌈ \sqrt{M} ⌉$ with actual marked probability at least $1 - 1 / M$ . The recurrence probabilities in [F1] equal these actual probabilities by [F3], so their finite maximizing choice has probability no smaller than that candidate. The $N = 1$ case already has probability one by step 1.1.

3.1F2F5step 2.1algebra∎

The simulation in [F2] makes the algorithm's padded Grover evolution exactly the evolution analyzed in step 2.1. Initializing the verification response to $0$ makes its XOR output equal to the queried bit. On a one-mark input, a marked measurement is valid and the final verification returns $1$ , so the algorithm returns the correct marked coordinate with probability at least the bound from step 2.1. On $0^{N}$ , every verification query returns $0$ , so it returns no with certainty. Finally $M \geq N$ implies $1 - 1 / M \geq 1 - 1 / N$ .

Depends on

Used by

Bounded-error unstructured search query complexity is Theta of square root N Theorem

Dependency tree · two levels

34 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

Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp, Quantum Amplitude Amplification and Estimation (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (2025) (standard reference, not scraped)