LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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-rational Legendre criterion before the terminal convergent

Statement

Let $A, p \in Z$ and $D, q \in Z_{> 0}$ , with $A / D$ and $p / q$ reduced and $D > 2 q$ . If $∣ A / D - p / q ∣ < 1 / (2 q^{2})$ , then $p / q$ is a convergent of the normalized finite regular continued fraction of $A / D$ . This is a finite-rational statement; it does not invoke the irrational-input Legendre theorem.

Facts & Assumptions

Given: Reduced $A / D$ with $D > 2 q$ , and reduced $p / q$ with $q > 0$ and $∣ A / D - p / q ∣ < 1 / (2 q^{2})$ .

[F1]

A rational continued fraction terminates at its Euclidean quotient list, and normalized finite expansion chooses the representation whose last digit is at least $2$ unless the expansion is an integer (The continued-fraction algorithm terminates exactly on rational numbers, Normalized finite regular continued fractions are unique).

[F2]

For convergents, $p_{n} = a_{n} p_{n - 1} + p_{n - 2}$ and $q_{n} = a_{n} q_{n - 1} + q_{n - 2}$ , and the finite-prefix formula is $(T p_{j} + p_{j - 1}) / (T q_{j} + q_{j - 1})$ for the positive remaining tail $T$ (Convergents of a regular continued fraction, Convergents are given by the standard recurrences and tail formula, Complete-quotient tail formula).

[F3]

Adjacent convergents satisfy $p_{j} q_{j - 1} - p_{j - 1} q_{j} = (- 1)^{j - 1}$ (Determinant identity for consecutive convergents).

[F4]

The complete quotient is $T = a_{j + 1}$ at the last digit and otherwise $T > a_{j + 1}$ ; the denominator recurrence is increasing after the possible initial equality $q_{0} = q_{1} = 1$ (Complete quotients in the continued-fraction algorithm, Convergents of a regular continued fraction).

[F5]

Reduced means coprime numerator and positive denominator, with gcd $1$ . If $d$ is coprime to $u$ and $d ∣ u v$ , then $d ∣ v$ (Coprime integers: $\gcd (a, b) = 1$ , If $\gcd (a, b) = 1$ and $a ∣ b c$ then $a ∣ c$ ; and if $a ∣ c$ , $b ∣ c$ and $\gcd (a, b) = 1$ then $a b ∣ c$ ). Rational absolute value is multiplicative and satisfies the triangle inequality (Absolute value and the triangle inequality).

Proof

1.1givenF1F2F3F5algebra

By [F1], write $A / D = [a_{0}; \dots, a_{s}]$ in normalized finite form. Since $D > 2 q \geq 2$ , $A / D$ is not an integer, so $s \geq 1$ . Its terminal convergent equals $A / D$ by [F1] and [F2]. By [F3], any common divisor of $p_{s}, q_{s}$ divides $1$ , so this pair is coprime. Cross multiplication gives $A q_{s} = p_{s} D$ . Since $\gcd (A, D) = 1$ , [F5] gives $D ∣ q_{s}$ ; since $\gcd (p_{s}, q_{s}) = 1$ , it also gives $q_{s} ∣ D$ . Both denominators are positive, so they are equal: $q_{s} = D$ .

2.1givenF2step 1.1algebra

If $q = 1$ , then $p$ is an integer and $∣ A / D - p ∣ < 1 / 2$ . Put $a_{0} = ⌊ A / D ⌋$ and $e : = A / D - a_{0} \in (0, 1)$ . The only possible such integers are $a_{0}$ and $a_{0} + 1$ . The first is the zeroth convergent. If $p = a_{0} + 1$ , then $e > 1 / 2$ , hence $a_{1} = ⌊ 1 / e ⌋ = 1$ ; the recurrence in [F2] gives $p_{1} / q_{1} = (a_{0} + 1) / 1$ . Thus $p / q$ is a convergent.

2.2givenF2F4step 1.1choose

Suppose $q \geq 2$ . Since $q < D = q_{s}$ , choose the largest $j$ with $q_{j} \leq q$ . Then $0 \leq j < s$ ; the only repeated initial denominator can be $q_{0} = q_{1} = 1$ , so $q_{j} > 0$ and $s_{0} : = q_{j - 1} / q_{j}$ lies in $[0, 1]$ (with $q_{- 1} = 0$ when $j = 0$ ). Put $T = a_{j + 1}$ if $j + 1 = s$ , and otherwise let $T$ be the complete quotient after the prefix. By [F4], $T \geq a_{j + 1}$ , and $x : = q / q_{j}$ satisfies $1 \leq x < a_{j + 1} + s_{0} \leq T + s_{0} = : L$ .

3.1F2F3F5step 2.2algebra

Put $ε = p_{j} q_{j - 1} - p_{j - 1} q_{j} = \pm 1$ by [F3]. The integers $u = ε (q_{j - 1} p - p_{j - 1} q)$ and $v = ε (p_{j} q - q_{j} p)$ satisfy $(p, q) = u (p_{j}, q_{j}) + v (p_{j - 1}, q_{j - 1})$ by expansion and $ε^{2} = 1$ ; hence $x = u + v s_{0}$ . Cross multiplication using the tail formula [F2] gives $\frac{p}{q} - \frac{A}{D} = \frac{(u p_{j} + v p_{j - 1}) (T q_{j} + q_{j - 1}) - (T p_{j} + p_{j - 1}) (u q_{j} + v q_{j - 1})}{q (T q_{j} + q_{j - 1})} = \frac{ε (u - v T)}{q_{j}^{2} x L}$ . Since $q = x q_{j}$ , it follows that $q^{2} ∣ A / D - p / q ∣ = x ∣ u - v T ∣ / L$ . Finally $L = T + s_{0}$ and $x = u + v s_{0}$ , so $u - v T = x - v L$ and $q^{2} ∣ A / D - p / q ∣ = x ∣ x - v L ∣ / L$ .

4.1givenstep 3.1algebra

The hypothesis makes the expression in step 3.1 less than $1 / 2$ . If $v \leq - 1$ , then $∣ x - v L ∣ \geq x + L$ , so $x ∣ x - v L ∣ / L > x \geq 1$ . If $v \geq 2$ , then $∣ x - v L ∣ \geq 2 L - x > L$ because $x < L$ , so again $x ∣ x - v L ∣ / L > x \geq 1$ . Both alternatives are impossible.

4.2givenF4step 2.2step 3.1algebra

If $v = 1$ , then $u = x - s_{0}$ is an integer. If $s_{0} < 1$ , $x \geq 1$ implies $u > 0$ ; if $s_{0} = 1$ , then $j \geq 1$ and $q_{j} = q_{j - 1} = 1$ , while $q \geq 2$ forces $x \geq 2$ . Thus $u \geq 1$ . Also $q < q_{j + 1}$ implies $u < a_{j + 1}$ , so $L - x = T - u \geq 1$ . Hence $x (L - x) / L \geq x / (x + 1) \geq 1 / 2$ , contradicting the strict hypothesis. Thus $v \neq 1$ .

5.1F1step 4.1step 4.2algebra∎

The alternatives $v \leq - 1$ , $v \geq 2$ , and $v = 1$ were excluded in steps 4.1–4.2, so $v = 0$ . Then $(p, q) = u (p_{j}, q_{j})$ , hence $p / q = p_{j} / q_{j}$ and $p / q$ is the $j$ th convergent. The proof includes the terminal case $j + 1 = s$ because only $T \geq a_{j + 1}$ was used, allowing equality at the terminal tail.

Depends on

Used by

Dependency tree · two levels

33 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

Andrew M. Childs, Lecture Notes on Quantum Algorithms, §9 (standard reference, not scraped)
Peter W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (standard reference, not scraped)