LemmaStatement: 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.

Terminating certified rounding for a counting estimate

Statement

Given integers $N \geq 1$ , even $M \geq 2$ , and $0 \leq y < M$ , let $z = N \sin^{2} (π y / M)$ . There is a terminating deterministic rational-interval procedure that produces an integer $q$ with $∣ q - z ∣ \leq 2 / 3$ . Its arithmetic work is a classical bit cost; no polynomial bit bound is asserted.

Facts & Assumptions

Given: Integers $N \geq 1$ , even $M \geq 2$ , and a phase label $0 \leq y < M$ .

[F1]

$3 < π < 22 / 7$ , and $π / 4 = \sum_{n = 0}^{\infty} (- 1)^{n} / (2 n + 1)$ . After $n$ terms, the alternating-series error gives $∣ π - 4 S_{n} ∣ \leq 4 / (2 n + 1)$ , where $S_{n} = \sum_{k < n} (- 1)^{k} / (2 k + 1)$ . Increasing $n$ until $8 / (2 n + 1)$ is below a requested rational width yields the rational interval $[4 S_{n} - 4 / (2 n + 1), 4 S_{n} + 4 / (2 n + 1)]$ ; termination follows from the Archimedean property (Rational bounds for pi used in finite schedules, Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series, The alternating series test: if $(b_{k})$ is nonincreasing with $b_{k} \to 0$ then $\sum_{k} (- 1)^{k} b_{k}$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_{n}$ , Every complete ordered field is Archimedean).

[F2]

Cosine is represented by its everywhere-convergent power series (Sine and cosine defined by their real power series).

[F3]

Rational arithmetic, interval comparison, and output writing are charged classical bit operations (Classical bit-operation cost).

[F4]

For $x = 2 π y / M$ and $ζ_{M} = e^{2 π i / M}$ , the exponential addition law gives $ζ_{M}^{\pm y} = e^{\pm i x}$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential). Euler's formula, $∣ e^{i x} ∣ = 1$ , and $e^{- i x} = (e^{i x})^{- 1}$ give $ζ_{M}^{y} + ζ_{M}^{- y} = 2 \cos x$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ). Together with [F5], this proves $\sin^{2} (π y / M) = (2 - ζ_{M}^{y} - ζ_{M}^{- y}) / 4$ for every integer $M \geq 2$ , including $M = 2$ and non-dyadic $M$ .

[F5]

The cosine double-angle identity gives $\cos (2 u) = 1 - 2 \sin^{2} u$ (Double-angle and quadratic power-reduction identities).

[F6]

For $x, y \in [0, 8]$ and $d \geq 1$ , factoring $x^{d} - y^{d} = (x - y) \sum_{j = 0}^{d - 1} x^{d - 1 - j} y^{j}$ gives $∣ x^{d} - y^{d} ∣ \leq d 8^{d - 1} ∣ x - y ∣$ .

[F7]

The alternating-series remainder bounds the tail by the first omitted term when magnitudes decrease to zero (The alternating series test: if $(b_{k})$ is nonincreasing with $b_{k} \to 0$ then $\sum_{k} (- 1)^{k} b_{k}$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_{n}$ ).

[F8]

For $R_{r} = 8^{2 r + 2} / (2 r + 2)!$ , $R_{r + 1} / R_{r} = 64 / ((2 r + 4) (2 r + 3)) \to 0$ . The ratio test gives convergence of $\sum_{r \geq 4} R_{r}$ , and the term test then gives $R_{r} \to 0$ (Ratio test: $lim sup ∣ a_{k + 1} / a_{k} ∣ < 1$ gives absolute convergence and hence convergence, and $lim inf ∣ a_{k + 1} / a_{k} ∣ > 1$ gives divergence, If a series converges then its terms tend to $0$ ).

[F9]

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

[F10]

The real absolute value is defined by $∣ x ∣ = x$ for $x \geq 0$ and $∣ x ∣ = - x$ for $x < 0$ (Absolute value in an ordered field).

[F11]

The exact rational-interval instructions, including the $y = 0$ branch, the $r$ and enclosure-index loops, and the output $q = ⌈ v - 2 / 3 ⌉$ for the final interval $[u, v]$ , are defined in Rational-interval rounding of a counting output.

Proof

1.1givenF1F2F6F7F11algebra

If $y = 0$ , [F11] returns $q = 0 = z$ , so assume $0 < y < M$ . Since $π < 22 / 7 < 4$ , the true argument $x = 2 π y / M$ lies in $(0, 8)$ . For any accepted enclosure index $h$ in [F11], write $x_{r} = x_{h}$ , $ρ_{r} = ρ_{h}$ and $I_{r} = [u, v]$ for its output interval. For every $r \geq 4$ , the cosine terms after index $r$ alternate with decreasing magnitudes, so the omitted tail is bounded by $R_{r}$ . For each integer $k \geq 1$ , [F6] bounds $∣ x^{2 k} - x_{r}^{2 k} ∣$ by $2 k 8^{2 k - 1} ∣ x - x_{r} ∣$ ; summing with the factorial coefficients gives $∣ C_{r} (x) - C_{r} (x_{r}) ∣ \leq D_{r} ρ_{r}$ . Thus $∣ \cos x - C_{r} (x_{r}) ∣ \leq D_{r} ρ_{r} + R_{r} = E$ , and the endpoints in [F11] enclose $z = N (1 - \cos x) / 2$ in $I_{r}$ .

2.1givenF1F8F11step 1.1algebra

The ratio of successive $R_{r}$ bounds tends to zero, so $R_{r} \to 0$ and a finite $r$ satisfies $N R_{r} < 1 / 24$ . For that $r$ , the enclosure-index loop in [F11] refines the alternating arctangent enclosure of $π$ until its propagated argument interval is contained in $[0, 8]$ and $N D_{r} ρ_{r} < 1 / 24 - N R_{r}$ : this terminates because the true argument is strictly inside $[0, 8]$ , $D_{r}$ is finite, and the enclosures become arbitrarily narrow. The cosine interval has width at most $2 (D_{r} ρ_{r} + R_{r})$ , so its $z$ interval has width $N (D_{r} ρ_{r} + R_{r}) < 1 / 24 < 1 / 6$ . Both loops terminate.

3.1givenF3F4F5F9F10F11step 2.1algebra∎

Apply [F9] to $z + 1 / 2$ and set $n = ⌊ z + 1 / 2 ⌋$ . Then $n \leq z + 1 / 2 < n + 1$ , so $- 1 / 2 \leq z - n < 1 / 2$ and [F10] gives $∣ z - n ∣ \leq 1 / 2$ . If $I_{r} = [u, v]$ contains $z$ and has width below $1 / 6$ , every $x \in I_{r}$ satisfies $- 1 / 6 < x - z < 1 / 6$ ; adding these bounds gives $- 2 / 3 < x - n < 2 / 3$ . Thus the closed radius- $2 / 3$ interval about $n$ contains all of $I_{r}$ , so an eligible integer exists. Eligibility is exactly $v - 2 / 3 \leq q \leq u + 2 / 3$ , so the least eligible integer is $q = ⌈ v - 2 / 3 ⌉$ , as returned by [F11]. It gives $∣ q - z ∣ \leq 2 / 3$ because $z \in I_{r}$ . All rational operations and output work are charged by [F3]. The identity $z = N \sin^{2} (π y / M)$ follows from the cosine double-angle identity, and its exact encoding is covered by [F4] using [F5].

Depends on

Used by

Relative approximate counting with unknown marked count Algorithm
Relative approximate counting success guarantee Theorem

Cited to discharge well-definedness by Rational-interval rounding of a counting output.

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

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)