§5, p. 1500 — the fraction near is a continued-fraction convergent of
ProvedShorAlgorithms.OrderFinding.fraction_is_convergentcontinued-fractionsnumber-theoryorder-findingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be natural numbers with , and let be a rational number whose denominator in lowest terms is smaller than and which satisfies
Then is one of the convergents of the continued fraction expansion of the real number .
This is why the continued fraction expansion of finds the fraction that the rounding step of the algorithm needs.
Formalization Note Convergents are Mathlib's Real.convergent. The polynomial running time of the continued fraction algorithm, also mentioned in the paper's sentence, is not stated.
Preamble
import Mathlib
Formal statement
namespace ShorAlgorithms.OrderFinding
/-- Shor (1997), §5, p. 1500: the fraction found by rounding is among the continued-fraction
convergents of `c/q`. If `n² ≤ q` and a rational `s` with lowest-terms denominator smaller
than `n` satisfies `|c/q - s| ≤ 1/(2q)`, then `s` is a convergent of the continued fraction
expansion of `c/q`. -/
theorem fraction_is_convergent (n q c : ℕ) (hnq : n ^ 2 ≤ q) (s : ℚ) (hs : s.den < n)
(h : |(c : ℝ) / q - (s : ℝ)| ≤ 1 / (2 * q)) :
∃ m : ℕ, s = ((c : ℝ) / q).convergent m := by sorry
end ShorAlgorithms.OrderFinding
Source
Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5) (1997), p. 1500, §5, "This fraction can be found in polynomial time by using a continued fraction expansion of c/q, which finds all the best approximations of c/q by fractions"
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.