Shor's reduction of factoring to order finding

TheoremShor's order-to-factor reduction#✓fully proved

Let \(N\), \(a\) and \(r\) be natural numbers with \(N > 1\) and \(a \ge 1\). Suppose \(a^r \equiv 1 \pmod{N}\), \(r\) is even, \(a^{r/2} \not\equiv 1 \pmod{N}\) and \(a^{r/2} \not\equiv -1 \pmod{N}\). Then \(d = \gcd(a^{r/2} - 1, N)\), the value computed by the classical post-processing, is a nontrivial factor of \(N\): \(d\) divides \(N\) and \(1 < d < N\).

In the algorithm \(r\) is the multiplicative order of \(a\) modulo \(N\), so the hypothesis \(a^{r/2} \not\equiv 1 \pmod{N}\) is the minimality of the order, and the hypothesis \(a^{r/2} \not\equiv -1 \pmod{N}\) is the "good unit" condition. This module assumes that condition; it does not prove its prevalence among units.

theorem gcd_factor_of_order {N a r : ℕ} (hN : 1 < N) (ha : 1 ≤ a)
    (hord : N ∣ a ^ r - 1) (hr : Even r)
    (hne1 : ¬ N ∣ a ^ (r / 2) - 1) (hnem1 : ¬ N ∣ a ^ (r / 2) + 1) :
    Nat.gcd (a ^ (r / 2) - 1) N ∣ N ∧ 1 < Nat.gcd (a ^ (r / 2) - 1) N ∧
      Nat.gcd (a ^ (r / 2) - 1) N < N

Sources

• P. W. Shor, Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer, SIAM J. Comput. 26 (1997), 1484–1509, Section 5; M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Section 5.3.

Used by 1

Used byShor's order-to-factor reduction, existential form

TheoremShor's order-to-factor reduction, existential form#✓fully proved

Let \(N\), \(a\) and \(r\) be natural numbers with \(N > 1\) and \(a \ge 1\). If \(a^r \equiv 1 \pmod{N}\), \(r\) is even, \(a^{r/2} \not\equiv 1 \pmod{N}\) and \(a^{r/2} \not\equiv -1 \pmod{N}\), then \(N\) has a nontrivial factor: there is a natural number \(d\) with \(d \mid N\) and \(1 < d < N\).

One such factor is \(\gcd(a^{r/2} - 1, N)\).

theorem exists_factor_of_order {N a r : ℕ} (hN : 1 < N) (ha : 1 ≤ a)
    (hord : N ∣ a ^ r - 1) (hr : Even r)
    (hne1 : ¬ N ∣ a ^ (r / 2) - 1) (hnem1 : ¬ N ∣ a ^ (r / 2) + 1) :
    ∃ d, d ∣ N ∧ 1 < d ∧ d < N

Uses 1

Proof usesShor's order-to-factor reduction

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.