Register size: $\frac{1}{2^{2n+1}} \le \frac{1}{2N^2} \le \frac{1}{2r^2}$

Proved

ShorWiki.register_size_bound

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-computingshor-algorithm

Let $1 < a < N$ with $\gcd(a,N)=1$ , $r = \operatorname{ord}_N(a)$ and $n = \lceil\log_2 N\rceil$ . Then

\frac{1}{2^{2n+1}} \;\le\; \frac{1}{2N^2} \;\le\; \frac{1}{2r^2}.

This is why a first register of $2n$ qubits suffices: an optimal outcome $k$ approximates $j/r$ to within $1/2^{2n+1}$ , which is within the range of the continued fraction theorem.

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem register_size_bound (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hcop : Nat.Coprime a N) :
    (1 : ℝ) / 2 ^ (2 * regBits N + 1) ≤ 1 / (2 * (N : ℝ) ^ 2) ∧
      1 / (2 * (N : ℝ) ^ 2) ≤ 1 / (2 * (ord N a : ℝ) ^ 2) := by sorry

end ShorWiki

Source

Wikipedia, "Shor's algorithm", revision oldid=1378862216, https://en.wikipedia.org/w/index.php?title=Shor%27s_algorithm&oldid=1378862216, section "Choosing the size of the first register" (PDF p. 6)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Register size: 122n+1≤12N2≤12r2\frac{1}{2^{2n+1}} \le \frac{1}{2N^2} \le \frac{1}{2r^2}22n+11​≤2N21​≤2r21​

Register size: $\frac{1}{2^{2n+1}} \le \frac{1}{2N^2} \le \frac{1}{2r^2}$