Prove2Me

§5, p. 1501 — at least φ(r)\varphi(r) values of cc are good, and each one gives rr

Proved
ShorAlgorithms.OrderFinding.card_good_outcomes_ge

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryorder-findingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let n>1n > 1, let xx be coprime to nn with multiplicative order rr modulo nn, and let q=2lq = 2^l satisfy n2≤q<2n2n^2 \le q < 2n^2. Call c∈{0,…,q−1}c \in \{0, \dots, q-1\} good if there is 0≤d<r0 \le d < r with gcd⁡(d,r)=1\gcd(d, r) = 1 and

∣cq−dr∣≤12q.\left|\frac{c}{q} - \frac{d}{r}\right| \le \frac{1}{2q}.

Then:

  1. there are at least φ(r)\varphi(r) good values of cc, where φ\varphi is Euler's totient function;
  2. the powers xk mod nx^k \bmod n, 0≤k<r0 \le k < r, take exactly rr distinct values, so there are at least rφ(r)r\varphi(r) states ∣c,xk mod n⟩|c, x^k \bmod n\rangle with cc good;
  3. every good cc gives us rr: rounding c/qc/q to the nearest fraction with denominator smaller than nn returns a fraction with denominator rr in lowest terms;
  4. every good cc satisfies (5.12): −r/2≤rc−d′q≤r/2-r/2 \le rc - d'q \le r/2 for some integer d′d'.

Together with the per-state bound 1/3r21/3r^2, this gives at least rφ(r)r\varphi(r) outcomes ∣c,xk⟩|c, x^k\rangle, each of probability at least 1/3r21/3r^2 and each of which yields rr.

Formalization Note "Gives us rr" is yieldsOrder n q r c. At r=1r = 1 the only dd is d=0d = 0 (since gcd⁡(0,1)=1\gcd(0,1) = 1), matching φ(1)=1\varphi(1) = 1. The hypothesis n>1n > 1 excludes n=1n = 1, where no fraction has denominator smaller than nn.

Preamble
import Mathlib
import Definitions.Def_ShorAlgorithms_OrderFinding_yieldsOrder
Formal statement
namespace ShorAlgorithms.OrderFinding

open Classical in
/-- Shor (1997), §5, pp. 1500–1501: the count of good observations. Let `n > 1`, `x` coprime
to `n` with order `r`, and `q = 2^l` with `n² ≤ q < 2n²`. Call `c ∈ {0, …, q-1}` *good* if
`|c/q - d/r| ≤ 1/(2q)` for some `0 ≤ d < r` relatively prime to `r`. Then
1. there are at least `φ(r)` good values of `c`;
2. there are `r` possible values `x^k (mod n)`, `0 ≤ k < r`, so there are at least `r φ(r)`
   states `|c, x^k (mod n)⟩` with `c` good; and
3. every good `c` gives us `r` by rounding (`yieldsOrder n q r c`) and satisfies (5.12),
   `-r/2 ≤ rc - d'q ≤ r/2` for an integer `d'`. -/
theorem card_good_outcomes_ge (n x q l : ℕ) (hn : 1 < n) (hx : Nat.Coprime x n)
    (hq : q = 2 ^ l) (hnq : n ^ 2 ≤ q) (hq2 : q < 2 * n ^ 2) :
    Nat.totient (orderOf (x : ZMod n)) ≤
        ((Finset.univ : Finset (Fin q)).filter (fun c : Fin q => ∃ d : ℕ, d < orderOf (x : ZMod n) ∧
          Nat.Coprime d (orderOf (x : ZMod n)) ∧
          |((c : ℕ) : ℝ) / q - (d : ℝ) / (orderOf (x : ZMod n) : ℝ)| ≤ 1 / (2 * q))).card ∧
    ((Finset.range (orderOf (x : ZMod n))).image (fun k : ℕ => (x : ZMod n) ^ k)).card =
        orderOf (x : ZMod n) ∧
    orderOf (x : ZMod n) * Nat.totient (orderOf (x : ZMod n)) ≤
        (((Finset.univ : Finset (Fin q)).filter (fun c : Fin q => ∃ d : ℕ, d < orderOf (x : ZMod n) ∧
          Nat.Coprime d (orderOf (x : ZMod n)) ∧
          |((c : ℕ) : ℝ) / q - (d : ℝ) / (orderOf (x : ZMod n) : ℝ)| ≤ 1 / (2 * q))) ×ˢ
          ((Finset.range (orderOf (x : ZMod n))).image (fun k : ℕ => (x : ZMod n) ^ k))).card ∧
    ∀ c : Fin q, (∃ d : ℕ, d < orderOf (x : ZMod n) ∧ Nat.Coprime d (orderOf (x : ZMod n)) ∧
          |((c : ℕ) : ℝ) / q - (d : ℝ) / (orderOf (x : ZMod n) : ℝ)| ≤ 1 / (2 * q)) →
      yieldsOrder n q (orderOf (x : ZMod n)) (c : ℕ) ∧
        ∃ d : ℤ,
          -((orderOf (x : ZMod n) : ℝ) / 2) ≤
            (orderOf (x : ZMod n) : ℝ) * ((c : ℕ) : ℝ) - (d : ℝ) * (q : ℝ) ∧
          (orderOf (x : ZMod n) : ℝ) * ((c : ℕ) : ℝ) - (d : ℝ) * (q : ℝ) ≤
            (orderOf (x : ZMod n) : ℝ) / 2 := 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), pp. 1500–1501, §5, "There are φ(r) possible values of d relatively prime to r … which would enable us to obtain r"
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph