§5, eq. (5.13) — at most one fraction with denominator within of
ProvedShorAlgorithms.OrderFinding.fraction_uniquediophantine-approximationnumber-theoryorder-findingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be natural numbers with . If and are rational numbers whose denominators in lowest terms are smaller than and which both satisfy
then .
So the fraction singled out by (5.13) is determined by and alone, which is what makes rounding a well-defined way to recover it.
Formalization Note The paper writes "Because ", but its choice of on p. 1498 only guarantees (with equality when is a power of ). The statement holds under , which is the hypothesis used here; this is the stronger theorem. The value is not required to be smaller than .
Preamble
import Mathlib
Formal statement
namespace ShorAlgorithms.OrderFinding
/-- Shor (1997), §5, eq. (5.13), p. 1500: if `n² ≤ q`, there is at most one fraction with
(lowest-terms) denominator smaller than `n` within `1/(2q)` of `c/q`. The page writes
"Because `q > n²`"; the choice of `q` on p. 1498 only gives `n² ≤ q`, and the claim holds
under that weaker hypothesis, which is what is stated here. -/
theorem fraction_unique (n q c : ℕ) (hnq : n ^ 2 ≤ q) (s₁ s₂ : ℚ)
(h₁ : s₁.den < n) (h₂ : s₂.den < n)
(hs₁ : |(c : ℚ) / q - s₁| ≤ 1 / (2 * q)) (hs₂ : |(c : ℚ) / q - s₂| ≤ 1 / (2 * q)) :
s₁ = s₂ := 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, eq. (5.13) and "Because q > n^2, there is at most one fraction d/r with r < n that satisfies the above inequality"
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.