ExampleConstruction: Literature-sourcedVerification: 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.

Denominator-bounded reconstruction at the strict boundary

Example

Take $N = 2$ , $Q = 17$ , and $y = 9$ . The reconstruction hypothesis holds because $17 > 4 (2)^{2} = 16$ . The normalized continued fraction is $\frac{9}{17} = [0; 1, 1, 8],$ with convergents $0 / 1, 1 / 1, 1 / 2, 9 / 17$ . For $p / q = 1 / 2$ , the exact comparison is $2 ∣ y q - p Q ∣ = 2 ∣ 18 - 17 ∣ = 2 = q,$ so the candidate is accepted at equality. The integer comparison has no tolerance parameter.

Facts & Assumptions

Given: The exact candidate test from Denominator-bounded rational phase reconstruction, the finite rational criterion, and the uniqueness result.

[F1]

A candidate has reduced denominator $1 \leq q \leq N$ and passes exactly when $2 ∣ y q - p Q ∣ \leq q$ (Denominator-bounded rational phase reconstruction).

[F2]

A rational has a terminating continued-fraction algorithm, and each finite convergent is the recurrence-defined fraction $p_{j} / q_{j}$ (The continued-fraction algorithm terminates exactly on rational numbers, Convergents of a regular continued fraction).

[F3]

For $Q > 4 N^{2}$ , at most one reduced fraction with denominator at most $N$ passes this test (Uniqueness of denominator-bounded phase candidates).

[F4]

The finite-rational Legendre criterion assumes the strict inequality $∣ A / D - p / q ∣ < 1 / (2 q^{2})$ (Finite-rational Legendre criterion before the terminal convergent).

Proof

1.1givenF1F2algebra

The Euclidean divisions $17 = 1 \cdot 9 + 8$ , $9 = 1 \cdot 8 + 1$ , and $8 = 8 \cdot 1$ give the displayed normalized expansion and its convergents by [F2]. The denominator- $2$ convergent $1 / 2$ satisfies the exact equality in [F1], so it passes.

2.1F1F2F3F4step 1.1algebra∎

The other denominator- $1$ convergents fail: for $0 / 1$ , $2 ∣ 9 ∣ = 18 > 1$ ; for $1 / 1$ , $2 ∣ 9 - 17 ∣ = 16 > 1$ . The terminal fraction has denominator $17 > N$ and is excluded. Thus $1 / 2$ is the only candidate; this also follows from [F3]. The algorithm's weak inequality accepts the tie, while [F4] uses a separate strict approximation hypothesis and is not invoked to turn equality into strictness.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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