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.

Correctness of phase-sample rational reconstruction

Statement

Let integers $N \geq 1$ , $m \geq 0$ , $Q = 2^{m}$ , and $1 \leq r \leq N$ satisfy $Q > 4 N^{2}$ , and let $k \in Z$ with $0 \leq k < r$ and $\gcd (k, r) = 1$ . Let $y \in {0, \dots, Q - 1}$ be any nearest grid label to phase $k / r$ in circular distance, meaning $\min_{z \in Z} ∣ k / r - y / Q - z ∣ \leq 1 / (2 Q)$ . Then Rational reconstruction from a phase sample returns $k / r$ . For every phase label $y$ , there is at most one passing candidate with denominator at most $N$ .

Facts & Assumptions

Given: Reduced $k / r \in [0, 1)$ with $r \leq N$ , $Q = 2^{m} > 4 N^{2}$ for an integer $m \geq 0$ , and a nearest circular grid label $y$ .

[F1]

Circular distance is $d_{T} (θ, y / Q) = \min_{z \in Z} ∣ θ - y / Q - z ∣$ ; for $θ \in [0, 1)$ , a nearest label has distance at most $1 / (2 Q)$ (Circular phase distance modulo one).

[F2]

The reconstruction routine tests the exact condition $2 ∣ y q - p Q ∣ \leq q$ on normalized finite-CF convergents with $q \leq N$ (Rational reconstruction from a phase sample, Denominator-bounded rational phase reconstruction).

[F3]

For reduced $A / D$ with $D > 2 q$ , a reduced $p / q$ satisfying $∣ A / D - p / q ∣ < 1 / (2 q^{2})$ is a convergent of the normalized finite expansion (Finite-rational Legendre criterion before the terminal convergent).

[F4]

At most one reduced fraction of denominator at most $N$ passes the exact reconstruction window when $Q > 4 N^{2}$ (Uniqueness of denominator-bounded phase candidates).

Proof

1.1givenF2F4algebra

If $k = 0$ , reducedness forces $r = 1$ . The only nearest circular grid label is $y = 0$ , so $y / Q = 0$ and its normalized finite expansion is $[0]$ with terminal convergent $0 / 1$ . This convergent has denominator $1 \leq N$ and passes the exact test, so [F2] and [F4] return $0 / 1 = k / r$ .

1.2givenF1algebra

Suppose $k > 0$ . The distance from $k / r$ to either endpoint $0, 1$ is at least $1 / r \geq 1 / N > 1 / (2 Q)$ , by $Q > 4 N^{2}$ . Therefore a nearest circular label cannot cross an endpoint: if $y / Q$ were on the other side of $0$ or $1$ , the circular distance would be at least the distance of $k / r$ from that endpoint, contradicting [F1]. Thus $∣ y / Q - k / r ∣ \leq 1 / (2 Q)$ .

2.1givenF2F4step 1.2algebra

Reduce $y / Q$ to $A / D$ with $D > 0$ . If $A / D = k / r$ , its normalized finite expansion terminates at that fraction; its terminal convergent is $k / r$ , whose denominator is at most $N$ , and step 1.2 gives $2 ∣ y r - k Q ∣ \leq r$ . Thus it passes [F2], and uniqueness [F4] makes the algorithm return it.

2.2givenF3step 1.2algebra

If $A / D \neq k / r$ , then $∣ A r - k D ∣$ is a positive integer, so $∣ A / D - k / r ∣ \geq 1 / (D r)$ . Combining with step 1.2 gives $D \geq 2 Q / r > 8 N^{2} / r \geq 8 r > 2 r$ , because $r \leq N$ . Also $Q > 4 N^{2} \geq 4 r^{2}$ gives $∣ A / D - k / r ∣ \leq 1 / (2 Q) < 1 / (8 r^{2}) < 1 / (2 r^{2})$ . Applying [F3] with $p / q = k / r$ shows it is a convergent of $A / D$ .

3.1F2F4step 1.2step 2.1step 2.2algebra∎

The same linear error bound in step 1.2 gives $2 ∣ y r - k Q ∣ \leq r$ . Therefore this convergent passes the exact test and denominator bound in [F2]. By [F4] it is the unique accepted candidate, so the algorithm returns $k / r$ . The two cases establish correctness and candidate uniqueness.

Depends on

Used by

Dependency tree · two levels

23 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

Peter W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)