The AKS primality criterion

Agrawal, Kayal and Saxena's polynomial identity generalizes Fermat's little theorem: for n ≥ 2 and a coprime to n, n is prime exactly when (X + a)^n = X^n + a in (ℤ / n)[X] (Cslib.AKS.prime_iff_add_pow_eq) Agrawal, Kayal, Saxena, Lemma 2.1. If n is prime, the identity is the Frobenius endomorphism together with a^n = a. If n is composite with a prime factor q < n, the coefficient C(n, q) a^{n - q} of X^q is nonzero modulo n, because q · C(n, q) = n · C(n - 1, q - 1) and Lucas's theorem gives C(n - 1, q - 1) ≡ 1 (mod q).

Checking the identity directly takes n coefficients. The AKS algorithm checks it only modulo X^r - 1, for a small r, and for a few values of a. Given r, the algorithm outputs PRIME exactly when n is not a perfect power, no a ≤ r has 1 < gcd(a, n) < n, and either n ≤ r or (X + a)^n ≡ X^n + a (mod X^r - 1, n) for every 1 ≤ a ≤ ⌊√φ(r) log₂ n⌋ (Cslib.AKS.Passes). Every prime passes, for every r (Cslib.AKS.passes_of_prime): this is the easy direction of Agrawal, Kayal, Saxena, Theorem 4.1. The converse, for r with multiplicative order of n modulo r above log₂² n, is the substance of their theorem.

Main definitions

• Cslib.AKS.IsPerfectPower: n = a ^ b for some b > 1.
• Cslib.AKS.numTests: the number ⌊√φ(r) log₂ n⌋ of tested values of a.
• Cslib.AKS.Congruence: (X + a)^n ≡ X^n + a (mod X^r - 1, n).
• Cslib.AKS.Passes: the conditions under which the AKS algorithm, given r, outputs PRIME.

Main results

• Cslib.AKS.not_dvd_choose_of_prime_dvd: a composite n does not divide C(n, q) for a prime factor q < n.
• Cslib.AKS.prime_iff_add_pow_eq: the AKS identity characterizes primes.
• Cslib.AKS.passes_of_prime: every prime passes the AKS tests.

References

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

The polynomial identity

theorem Cslib.AKS.not_dvd_choose_of_prime_dvd {n q : ℕ} (hq : Nat.Prime q) (hqn : q ∣ n) (hlt : q < n) : ¬n ∣ n.choose q

For a prime factor q < n of n, n does not divide C(n, q). Indeed n · C(n - 1, q - 1) = q · C(n, q), and C(n - 1, q - 1) ≡ 1 (mod q) by Lucas's theorem, since n - 1 ≡ q - 1 (mod q).

theorem Cslib.AKS.add_pow_eq_of_prime {p : ℕ} (hp : Nat.Prime p) (a : ZMod p) : (Polynomial.X + Polynomial.C a) ^ p = Polynomial.X ^ p + Polynomial.C a

Freshman's dream modulo a prime. For a prime p, (X + a)^p = X^p + a in (ℤ / p)[X].

theorem Cslib.AKS.prime_of_add_pow_eq {n : ℕ} (hn : 2 ≤ n) {a : ZMod n} (ha : IsUnit a) (h : (Polynomial.X + Polynomial.C a) ^ n = Polynomial.X ^ n + Polynomial.C a) : Nat.Prime n

If (X + a)^n = X^n + a in (ℤ / n)[X] for a unit a and n ≥ 2, then n is prime: for a prime factor q < n, the coefficient a^{n - q} C(n, q) of X^q would vanish.

theorem Cslib.AKS.prime_iff_add_pow_eq {n : ℕ} (hn : 2 ≤ n) {a : ZMod n} (ha : IsUnit a) : Nat.Prime n ↔ (Polynomial.X + Polynomial.C a) ^ n = Polynomial.X ^ n + Polynomial.C a

The AKS identity Agrawal, Kayal, Saxena, Lemma 2.1: for n ≥ 2 and a unit a of ℤ / n, n is prime exactly when (X + a)^n = X^n + a in (ℤ / n)[X].

The tests of the AKS algorithm

def Cslib.AKS.IsPerfectPower (n : ℕ) : Prop

n is a perfect power: n = a ^ b for some a and some b > 1.

noncomputable def Cslib.AKS.numTests (n r : ℕ) : ℕ

The number ⌊√φ(r) log₂ n⌋ of values of a for which the AKS algorithm tests its congruence.

def Cslib.AKS.Congruence (n r a : ℕ) : Prop

The AKS congruence (X + a)^n ≡ X^n + a (mod X^r - 1, n), stated in the quotient ring (ℤ / n)[X] / (X^r - 1).

def Cslib.AKS.Passes (n r : ℕ) : Prop

The conditions under which the AKS algorithm outputs PRIME, given r Agrawal, Kayal, Saxena, Section 4: n is not a perfect power (step 1), no a ≤ r has 1 < gcd(a, n) < n (step 3), and either n ≤ r (step 4) or the congruence holds for every 1 ≤ a ≤ ⌊√φ(r) log₂ n⌋ (step 5). The algorithm chooses r as the least number for which the multiplicative order of n modulo r exceeds log₂² n (step 2).

theorem Cslib.AKS.not_isPerfectPower_of_prime {p : ℕ} (hp : Nat.Prime p) : ¬IsPerfectPower p

A prime is not a perfect power.

theorem Cslib.AKS.congruence_of_prime {p : ℕ} (hp : Nat.Prime p) (r a : ℕ) : Congruence p r a

The AKS identity for a prime holds modulo X^r - 1.

theorem Cslib.AKS.passes_of_prime {p : ℕ} (hp : Nat.Prime p) (r : ℕ) : Passes p r

Every prime passes the AKS tests, for every r: the easy direction of Agrawal, Kayal, Saxena, Theorem 4.1.