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.

Finite exact comparison of real cyclotomic values

Statement

For an integer $s \geq 2$ , let $ζ_{s} = e^{2 π i / s}$ and let $P, R \in Q [X]$ be given coefficient lists such that $P (ζ_{s})$ and $R (ζ_{s})$ are real. There is a terminating deterministic exact procedure to decide which of these two real numbers is larger, or whether they are equal. Its bit-operation cost is charged to the classical cost model; no polynomial bound is asserted.

Facts & Assumptions

Given: The integer $s \geq 2$ , rational polynomials $P, R$ , and the promise that their values at $ζ_{s} = e^{2 π i / s}$ are real.

[F1]

The cyclotomic polynomial $Φ_{s}$ is irreducible over $Q$ and is the minimal polynomial of a primitive $s$ th root ( $Φ_{n}$ is irreducible in $Q [t]$ for every $n \geq 1$ ).

[F2]

Write $S_{n} = \sum_{j = 0}^{n - 1} (- 1)^{j} / (2 j + 1)$ . The arctangent theorem gives $π / 4 = \lim_{n} S_{n}$ , and the alternating-series test gives $∣ π / 4 - S_{n} ∣ \leq 1 / (2 n + 1)$ . For any rational width $η > 0$ , increasing $n$ until $8 / (2 n + 1) < η$ gives the rational interval $[4 S_{n} - 4 / (2 n + 1), 4 S_{n} + 4 / (2 n + 1)]$ of width below $η$ containing $π$ ; exact rational comparisons suffice, and the loop terminates because the natural numbers are unbounded (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).

[F3]

Sine and cosine are given by their convergent power series (Sine and cosine defined by their real power series).

[F4]

Rational arithmetic and exact comparisons are part of the separately charged classical bit-operation model (Classical bit-operation cost).

[F5]

$e^{i x} = \cos x + i \sin x$ for real $x$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F6]

For an alternating series whose nonnegative terms decrease to zero, the remainder after $r$ terms is at most the first omitted term (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}$ ).

Proof

1.1givenF1algebra

Form $D = P - R$ and divide it by $Φ_{s}$ over $Q$ . By irreducibility in [F1], $D (ζ_{s}) = 0$ exactly when the remainder is the zero polynomial; that finite rational coefficient test decides equality.

2.1givenF2F3F5F6step 1.1algebra

If the remainder is nonzero, then $d = D (ζ_{s})$ is a nonzero real algebraic number. Put $α = 2 π / s \in (0, 4)$ , using $s \geq 2$ and $π < 22 / 7 < 4$ . For any rational tolerance $η > 0$ , refine the pi enclosure from [F2] until the scaled interval $J$ for $α$ lies in $[0, 4]$ and has width below $η$ ; this terminates because $α \in (0, 4)$ . For $k \geq 4$ and $x \in [0, 4]$ , successive cosine-term magnitudes have ratio at most $16 / ((2 k + 2) (2 k + 1)) < 1$ , and successive sine-term magnitudes have ratio at most $16 / ((2 k + 3) (2 k + 2)) < 1$ . Thus [F3] and [F6] bound the cosine and sine tails after truncation through index $r \geq 4$ by $4^{2 r + 2} / (2 r + 2)!$ and $4^{2 r + 3} / (2 r + 3)!$ . The ratios of these bounds at successive $r$ are $16 / ((2 r + 4) (2 r + 3))$ and $16 / ((2 r + 5) (2 r + 4))$ , both below $1 / 2$ for $r \geq 4$ , so exact rational comparisons find an $r$ with both bounds below $η$ . For this fixed $r$ , refine $J$ until the rational interval evaluations of both truncation polynomials have widths below $η$ ; this exact test terminates because they are fixed polynomials and interval addition and multiplication preserve shrinking widths. Use those intervals with the alternating remainders to enclose $\cos α$ and $\sin α$ , then evaluate $D$ using rational complex interval arithmetic and Euler's formula [F5]. The resulting real intervals contain $d$ and have widths tending to zero as $η \to 0$ , since each sine/cosine interval width and tail bound tends to zero and $D$ is a finite polynomial.

3.1givenF4step 1.1step 2.1algebra∎

Because $d \neq 0$ , its distance from zero is positive. Repeatedly refine the rational interval from step 2.1 until it lies strictly above or below zero; convergence of the interval widths guarantees finite termination, and its sign decides the strict order. Equality was already decided in step 1.1, so this procedure terminates on every promised input. Its finitely many rational operations are charged under [F4].

Depends on

Used by

Dependency tree · two levels

70 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)