Classical reduction: $\gcd(N, a^{r/2} \mp 1)$ are nontrivial factors when $N \nmid a^{r/2}+1$

Proved

ShorWiki.gcd_pow_half_nontrivial

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

quantum-computingshor-algorithm

Let $1 < a < N$ with $\gcd(a, N) = 1$ and let $r = \operatorname{ord}_N(a)$ . Suppose $r$ is even and $N \nmid a^{r/2} + 1$ . Then both

d = \gcd\!\left(N,\ a^{r/2} - 1\right) \quad\text{and}\quad d' = \gcd\!\left(N,\ a^{r/2} + 1\right)

are nontrivial factors of $N$ :

1 < d < N, \qquad 1 < d' < N .

This is the success criterion of Shor's algorithm: an even order with $a^{r/2} \not\equiv -1 \pmod N$ splits $N$ by a single gcd computation.

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem gcd_pow_half_nontrivial (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hcop : Nat.Coprime a N) (heven : Even (ord N a))
    (hndvd : ¬ N ∣ a ^ (ord N a / 2) + 1) :
    (1 < Nat.gcd N (a ^ (ord N a / 2) - 1) ∧ Nat.gcd N (a ^ (ord N a / 2) - 1) < N) ∧
      (1 < Nat.gcd N (a ^ (ord N a / 2) + 1) ∧ Nat.gcd N (a ^ (ord N a / 2) + 1) < N) := 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 "Classical reduction" (PDF p. 3) and restated algorithm, step 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

Classical reduction: gcd⁡(N,ar/2∓1)\gcd(N, a^{r/2} \mp 1)gcd(N,ar/2∓1) are nontrivial factors when N∤ar/2+1N \nmid a^{r/2}+1N∤ar/2+1

Classical reduction: $\gcd(N, a^{r/2} \mp 1)$ are nontrivial factors when $N \nmid a^{r/2}+1$