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.

Integer rounding gives a high-success Grover iterate

Statement

Put $a = t / N$ and $θ = \arcsin \sqrt{a}$ . If $0 < a \leq 1 / 2$ , some integer $k$ with $0 \leq k \leq K = ⌈ 1 / \sqrt{a} ⌉$ has $p_{k} = \sin^{2} ((2 k + 1) θ) \geq 1 - a .$ If $1 / 2 < a \leq 1$ , $k = 0$ lies in this range and $p_{0} = a > 1 / 2$ . The real-valued optimizer $k_{*} = π / (4 θ) - 1 / 2$ is not in general an integer.

Facts & Assumptions

Given: $N = 2^{n}$ , exact $t$ with $1 \leq t \leq N$ , $a = t / N$ , and $θ = \arcsin \sqrt{a}$ .

[F1]

Exact success probability after an integer number of Grover iterates: for $0 < t < N$ and each integer $k \geq 0$ , $p_{k} = \sin^{2} ((2 k + 1) θ)$ . For $t = N$ , every integer iteration count has marked probability $1$ .

[F2]

Principal inverse sine and inverse cosine: $\sin (\arcsin x) = x$ and $\arcsin x \in [- π / 2, π / 2]$ .

[F3]

Signs, monotonicity intervals, and ranges of sine and cosine: sine is strictly increasing on $[- π / 2, π / 2]$ , and cosine is strictly decreasing on $[0, π]$ .

[F4]

Sine and cosine are $1$ -Lipschitz on $R$ : $∣ \sin u - \sin v ∣ \leq ∣ u - v ∣$ .

[F5]

Quarter-turn values and shifts by pi/2 and pi: $\sin (π / 2) = 1$ and the sine/cosine shift identities by $π / 2$ hold.

[F7]

Double-angle and quadratic power-reduction identities: $\sin (2 x) = 2 \sin x \cos x$ .

[F8]

Parity and the Pythagorean identity for sine and cosine: sine is odd and $\sin^{2} x + \cos^{2} x = 1$ .

[F9]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : a nonnegative real has a unique nonnegative square root.

[F10]

Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ : every real $x$ has an integer $m = ⌊ x ⌋$ with $m \leq x < m + 1$ .

[F11]

Pi as twice the smallest positive zero of cosine and Cosine has a smallest positive zero, lying strictly between zero and two: $π = 2 γ$ with $0 < γ < 2$ , so $0 < π < 4$ .

[F12]

Ceilings give the least positive integer meeting a real threshold: $K = ⌈ 1 / \sqrt{a} ⌉$ is an integer at least $1 / \sqrt{a}$ .

[F13]

The derivatives of sine and cosine are cosine and minus sine: $\sin 0 = 0$ .

[F14]

Squaring is monotone on the nonnegatives: nonnegative square roots preserve order.

Proof

1.1givenF2F3F4F5F7F8F9F11F13F14algebra

Suppose $0 < a \leq 1 / 2$ . Put $x = π / 4$ , $s = \sin x$ , and $c = \cos x$ . By [F11], $0 < π < 4$ , so $0 < x < π / 2$ ; [F3] gives $s > 0$ , and its cosine monotonicity together with [F5] gives $c > \cos (π / 2) = 0$ . The double-angle identity [F7] and quarter-turn value [F5] give $2 s c = \sin (2 x) = \sin (π / 2) = 1$ , while [F8] gives $s^{2} + c^{2} = 1$ . Thus $(s - c)^{2} = s^{2} + c^{2} - 2 s c = 0$ , so $s = c$ ; hence $2 s^{2} = 1$ and $s = 1 / \sqrt{2}$ by [F9]. Since $a \leq 1 / 2$ , [F14] gives $\sqrt{a} \leq 1 / \sqrt{2} = s$ , and strict increase in [F3] implies $θ \leq π / 4$ . Also $\sin θ = \sqrt{a} > 0 = \sin 0$ , and $θ \in [- π / 2, π / 2]$ by [F2], so strict increase [F3] gives $θ > 0$ . The Lipschitz estimate [F4] then yields $\sqrt{a} = ∣ \sin θ - \sin 0 ∣ \leq ∣ θ ∣ = θ$ .

2.1step 1.1F2F3F10constructalgebra

Put $k_{*} = π / (4 θ) - 1 / 2$ . Since $θ \leq π / 4$ , $k_{*} \geq 1 / 2$ . Let $m = ⌊ k_{*} ⌋$ and choose $k = m$ if $k_{*} - m \leq 1 / 2$ , otherwise choose $k = m + 1$ . By [F10], $k$ is a nonnegative integer and $∣ k - k_{*} ∣ \leq 1 / 2$ . For $a = 1 / 2$ , the value of $\sin (π / 4)$ from step 1.1 and injectivity in [F3] give $θ = π / 4$ , hence $k_{*} = 1 / 2$ , exhibiting a noninteger optimizer.

3.1step 1.1step 2.1F11F12algebra

The choice in step 2.1 gives $k \leq k_{*} + 1 / 2 = π / (4 θ) \leq π / (4 \sqrt{a}) < 1 / \sqrt{a} \leq K$ , using [F11]–[F12].

3.2F1step 1.1step 2.1F2F3F5F8F11algebra

By the definition of $k_{*}$ , $(2 k_{*} + 1) θ = π / 2$ . Therefore $1 - p_{k} = \cos^{2} ((2 k + 1) θ) = \sin^{2} (2 (k - k_{*}) θ)$ . The angle magnitude is at most $θ \leq π / 4$ by step 2.1. Oddness and monotonicity of sine imply $∣ \sin (2 (k - k_{*}) θ) ∣ \leq \sin θ$ ; hence $1 - p_{k} \leq \sin^{2} θ = a$ and $p_{k} \geq 1 - a$ .

4.1givenF1F2F9F12algebra∎

If $1 / 2 < a < 1$ , then $K \geq 1$ and $k = 0$ is in the candidate range; [F1] and [F2] give $p_{0} = \sin^{2} θ = a > 1 / 2$ . If $a = 1$ , then $K = 1$ by [F12] and [F9], and the endpoint clause of [F1] gives $p_{0} = 1 = a > 1 / 2$ .

Depends on

Used by

Dependency tree · two levels

63 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, §7.2 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms, §19.1 (standard reference, not scraped)