Quantum order finding recovers the order $r$ with probability at least $\varphi(r)/3r$

Proved

ShorAlgorithms.OrderFinding.order_recovered_prob_ge

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

order-findingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1probabilityquantum-algorithms

There is a threshold $N$ such that the following holds for every $n \ge N$ . Let $x$ be coprime to $n$ and let $r$ be its multiplicative order modulo $n$ , the least $r \ge 1$ with $x^r \equiv 1 \pmod n$ . Let $q = 2^l$ be the power of $2$ with $n^2 \le q < 2n^2$ . Run Shor's order-finding procedure: prepare the state

\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle,

apply the Fourier transform $A_q$ to the first register, measure, and round $c/q$ to the nearest fraction with denominator smaller than $n$ . Then the probability that the observed $c$ gives us $r$ (the rounded fraction has denominator $r$ in lowest terms) is at least

\frac{\varphi(r)}{3r}.

This is the paper's main claim about the quantum part of the factoring algorithm; combined with $\varphi(r)/r > \delta/\log\log r$ , it shows that $O(\log\log r)$ repetitions find $r$ with high probability.

Formalization Note The probability of the event is $\sum_{c \text{ good}} \sum_{y \in \mathbb{Z}/n} |\Psi(c, y)|^2$ , where $\Psi$ is built by applying $A_q$ to the first register of (5.2); summing over all $y$ is exact, since values $y$ that are not powers of $x$ have probability $0$ . "Gives us $r$ " is yieldsOrder. The threshold $N$ comes first and is uniform in $x$ and $q$ ; it is inherited from the paper's per-state bound, which holds "for sufficiently large $n$ ". [NeZero n] makes $\mathbb{Z}/n$ finite.

Preamble

import Mathlib
import Definitions.Def_ShorAlgorithms_OrderFinding_outcomeProb
import Definitions.Def_ShorAlgorithms_OrderFinding_yieldsOrder

Formal statement

namespace ShorAlgorithms.OrderFinding

open Classical in
/-- Shor (1997), §5, p. 1501 (goal). For all sufficiently large `n` (threshold `N` uniform in
`x` and `q`): let `x` be coprime to `n` with order `r`, and `q = 2^l` with `n² ≤ q < 2n²`.
Run the order-finding algorithm (state (5.2), Fourier transform `A_q` on the first register,
measurement). The probability that the observed `c` gives us `r` by rounding `c/q` to the
nearest fraction with denominator smaller than `n` is at least `φ(r)/(3r)`. -/
theorem order_recovered_prob_ge : ∃ N : ℕ, ∀ (n : ℕ) [NeZero n], N ≤ n →
    ∀ x : ℕ, Nat.Coprime x n → ∀ q l : ℕ, q = 2 ^ l → n ^ 2 ≤ q → q < 2 * n ^ 2 →
    (Nat.totient (orderOf (x : ZMod n)) : ℝ) / (3 * (orderOf (x : ZMod n) : ℝ)) ≤
      ∑ c ∈ (Finset.univ : Finset (Fin q)).filter
          (fun c : Fin q => yieldsOrder n q (orderOf (x : ZMod n)) (c : ℕ)),
        ∑ y : ZMod n, outcomeProb n x q c y := 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. 1501, §5, "Since each of these states occurs with probability at least 1/3r^2, we obtain r with probability at least φ(r)/3r"; setup pp. 1498–1500

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

Quantum order finding recovers the order rrr with probability at least φ(r)/3r\varphi(r)/3rφ(r)/3r

Quantum order finding recovers the order $r$ with probability at least $\varphi(r)/3r$