Correctness of the AKS primality test

Theorem Agrawal, Kayal, Saxena, Theorem 4.1: if n ≥ 2 passes the tests of the AKS algorithm for an r such that the multiplicative order of n modulo r exceeds log₂² n, then n is prime (Cslib.AKS.prime_of_passes). Together with Cslib.AKS.passes_of_prime, the tests characterize the primes (Cslib.AKS.prime_iff_passes).

Proof

If n ≤ r, every a < n is coprime to n by step 3. Otherwise suppose n is composite with least prime factor p. Step 3 forces p > r. Let ζ be a primitive r-th root of unity in a field of characteristic p.

• Every m = (n/p)^i p^j is introspective for every product of the polynomials X + a, 0 ≤ a ≤ ⌊√φ(r) log₂ n⌋ (Cslib.AKS.Introspective).
• Let t be the number of residues of these m modulo r; log₂² n < ord_r(n) ≤ t ≤ φ(r). Put B = ⌊√t log₂ n⌋, so B < t and B ≤ ⌊√φ(r) log₂ n⌋.
• Lower bound. The products of B factors X + a with 0 ≤ a ≤ B take C(2B, B) distinct values at ζ: two products agreeing at ζ agree at the t distinct roots ζ^m, and have degree B < t.
• Upper bound. Since n is not a power of p, the numbers (n/p)^i p^j with i, j ≤ ⌊√t⌋ are distinct; there are more than t of them, so two, m₁ ≠ m₂, agree modulo r. Every value above is then a root of Y^{m₁} - Y^{m₂}, so there are at most n^{⌊√t⌋}.
• Finally n^{⌊√t⌋} ≤ n^{√t} < 2^{B + 1} ≤ C(2B, B), a contradiction.

This follows Agrawal, Kayal, Saxena, Section 4, with two simplifications: the field is generated by a primitive root of unity rather than by an irreducible factor of the cyclotomic polynomial, and the lower bound counts only products of exactly B factors.

Main results

• Cslib.AKS.prime_of_passes: correctness of the AKS tests.
• Cslib.AKS.prime_iff_passes: the AKS tests characterize the primes.

References

• M. Agrawal, N. Kayal, N. Saxena, PRIMES is in P

Elementary facts

theorem Cslib.AKS.prime_of_le_of_gcd {n r : ℕ} (hn : 2 ≤ n) (hgcd : ∀ (a : ℕ), 1 ≤ a → a ≤ r → a.gcd n = 1 ∨ a.gcd n = n) (hnr : n ≤ r) : Nat.Prime n

Step 4. If n ≤ r and no a ≤ r has 1 < gcd(a, n) < n, then n is prime.

theorem Cslib.AKS.coprime_of_orderOf_pos {n r : ℕ} (h : 0 < orderOf ↑n) : n.Coprime r

If n has positive multiplicative order modulo r, then n is coprime to r.

theorem Cslib.AKS.exists_eq_pow_of_pow_mul_pow_eq {p q i j i' j' : ℕ} (hp : Nat.Prime p) (hq : q ≠ 0) (hne : (i, j) ≠ (i', j')) (h : q ^ i * p ^ j = q ^ i' * p ^ j') : ∃ (s : ℕ), q = p ^ s

If q^i p^j = q^{i'} p^{j'} for distinct exponent pairs and a prime p, then q is a power of p.

Products of linear polynomials

noncomputable def Cslib.AKS.linProd (p : ℕ) {B : ℕ} (s : Sym (Fin (B + 1)) B) : Polynomial (ZMod p)

The product ∏_{a ∈ s} (X + a) over ℤ / p of a multiset s of B numbers in [0, B].

theorem Cslib.AKS.linProd_eq {p B : ℕ} (s : Sym (Fin (B + 1)) B) : linProd p s = (Multiset.map (fun (c : ZMod p) => Polynomial.X - Polynomial.C c) (Multiset.map (fun (a : Fin (B + 1)) => -↑↑a) ↑s)).prod

theorem Cslib.AKS.natDegree_linProd {p : ℕ} [Fact (Nat.Prime p)] {B : ℕ} (s : Sym (Fin (B + 1)) B) : (linProd p s).natDegree = B

theorem Cslib.AKS.linProd_injective {p : ℕ} [Fact (Nat.Prime p)] {B : ℕ} (hB : B < p) : Function.Injective (linProd p)

Distinct multisets give distinct products when B < p: the product determines its roots.

theorem Cslib.AKS.card_image_aeval_linProd {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] {r B : ℕ} [NeZero r] {ζ : K} (hζ : IsPrimitiveRoot ζ r) (hB : B < p) {S : Finset (ZMod r)} (hSB : B < S.card) (hS : ∀ x ∈ S, ∃ (m : ℕ), ↑m = x ∧ ∀ (s : Sym (Fin (B + 1)) B), Introspective K r m (linProd p s)) : (Finset.image (fun (s : Sym (Fin (B + 1)) B) => (Polynomial.aeval ζ) (linProd p s)) Finset.univ).card = B.centralBinom

The lower bound. Let S be a set of more than B residues modulo r, each the residue of a number introspective for every product ∏_{a ∈ s} (X + a). If B < p, these C(2B, B) products take distinct values at a primitive r-th root of unity ζ: two products agreeing at ζ agree at the |S| distinct roots ζ^m, and have degree B.

theorem Cslib.AKS.card_image_aeval_linProd_le {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] {r B : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ r) {m₁ m₂ : ℕ} (hne : m₁ ≠ m₂) (hmod : ↑m₁ = ↑m₂) (h₁ : ∀ (s : Sym (Fin (B + 1)) B), Introspective K r m₁ (linProd p s)) (h₂ : ∀ (s : Sym (Fin (B + 1)) B), Introspective K r m₂ (linProd p s)) : (Finset.image (fun (s : Sym (Fin (B + 1)) B) => (Polynomial.aeval ζ) (linProd p s)) Finset.univ).card ≤ max m₁ m₂

The upper bound. If distinct m₁ ≡ m₂ (mod r) are both introspective for every product ∏_{a ∈ s} (X + a), then every value of these products at a primitive r-th root of unity is a root of Y^{m₁} - Y^{m₂}, so there are at most max m₁ m₂ such values.

The theorem

theorem Cslib.AKS.prime_of_passes {n r : ℕ} (hn : 2 ≤ n) (hr : Real.logb 2 ↑n ^ 2 < ↑(orderOf ↑n)) (h : Passes n r) : Nat.Prime n

Correctness of the AKS tests Agrawal, Kayal, Saxena, Theorem 4.1: if n ≥ 2 passes the tests of the AKS algorithm for an r such that the multiplicative order of n modulo r exceeds log₂² n, then n is prime.

theorem Cslib.AKS.prime_iff_passes {n r : ℕ} (hn : 2 ≤ n) (hr : Real.logb 2 ↑n ^ 2 < ↑(orderOf ↑n)) : Nat.Prime n ↔ Passes n r

The AKS tests characterize the primes: for n ≥ 2 and r such that the multiplicative order of n modulo r exceeds log₂² n, n passes the tests of the AKS algorithm exactly when it is prime Agrawal, Kayal, Saxena, Theorem 4.1.