Classical reduction: $N \mid (a^{r/2}-1)(a^{r/2}+1)$ when the order $r$ is even

Proved

ShorWiki.dvd_pow_half_sub_one_mul_add_one

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)$ be the order of $a$ modulo $N$ . If $r$ is even, then

N \mid \left(a^{r/2} - 1\right)\left(a^{r/2} + 1\right).

This is the difference-of-squares factorisation of $a^r - 1$ , on which the classical reduction of factoring to order finding rests.

Formalization Note The statement is in natural numbers; since $a \ge 2$ , $a^{r/2} - 1$ involves no truncated subtraction.

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem dvd_pow_half_sub_one_mul_add_one (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hcop : Nat.Coprime a N) (heven : Even (ord N a)) :
    N ∣ (a ^ (ord N a / 2) - 1) * (a ^ (ord N a / 2) + 1) := 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)

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: N∣(ar/2−1)(ar/2+1)N \mid (a^{r/2}-1)(a^{r/2}+1)N∣(ar/2−1)(ar/2+1) when the order rrr is even

Classical reduction: $N \mid (a^{r/2}-1)(a^{r/2}+1)$ when the order $r$ is even