Classical reduction: if $\gcd(a,N) \ne 1$ then it is a nontrivial factor of $N$

Proved

ShorWiki.gcd_ne_one_nontrivial_factor

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

quantum-computingshor-algorithm

Let $1 < a < N$ be integers and let $K = \gcd(a, N)$ . If $K \ne 1$ , then $K$ is a nontrivial factor of $N$ :

K \mid N, \qquad 1 < K < N .

This is step 3 of the article's restated algorithm: before any quantum computation, a lucky choice of $a$ sharing a factor with $N$ already splits $N$ as $K \cdot (N/K)$ .

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem gcd_ne_one_nontrivial_factor (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hK : Nat.gcd a N ≠ 1) :
    Nat.gcd a N ∣ N ∧ 1 < Nat.gcd a N ∧ Nat.gcd a N < 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", restated algorithm, steps 1–3 (PDF p. 3)

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: if gcd⁡(a,N)≠1\gcd(a,N) \ne 1gcd(a,N)=1 then it is a nontrivial factor of NNN

Classical reduction: if $\gcd(a,N) \ne 1$ then it is a nontrivial factor of $N$