The polynomial congruence layer: the two Fermat congruences, introspection, and the set P
DefinitionAKS_polyThe polynomial layer of Agrawal, Kayal, and Saxena's "PRIMES is in P" (Annals of Mathematics 160 (2004) 781-793): the propositional content of Sections 2 and 4. Congruence (1) is the paper's generalization of Fermat's Little Theorem to polynomial rings: polyFermat n a states (X + a)^n = X^n + a as an equality in the polynomial ring over Z_n; by Lemma 2.1, for n at least 2 and a coprime to n, this holds exactly when n is prime. Congruence (2) reduces congruence (1) modulo X^r - 1: cycCong n r a states that X^r - 1 divides (X + a)^n - (X^n + a) in Z_n[X]; every prime satisfies it for all a and r, and the algorithm of Section 4 tests it for a single r and a range of a's. Definition 4.4 defines introspection: m is introspective for f when X^r - 1 divides f^m - f(X^m) over F_p. The set P collects the products of the generators X, X + 1, ..., X + ell over F_p, the multiplicatively closed family whose images in the field F_p[X]/(h) form the group G-cal of the paper's correctness proof.
import Mathlib /-! # The polynomial congruence layer: the two Fermat congruences and introspection The polynomial layer of the AKS mission, carrying the propositional content of Sections 2 and 4 of Agrawal, Kayal, and Saxena, "PRIMES is in P", Annals of Mathematics 160 (2004) 781-793: congruence (1), the polynomial generalization of Fermat's Little Theorem over Z_n[X]; congruence (2), its reduction modulo X^r - 1; Definition 4.4, the introspection relation over F_p[X]; and the set P of products of the generators X, X + 1, ..., X + l. -/ namespace AKS open Polynomial /-- Congruence (1) of the paper: (X + a)^n = X^n + a in Z_n[X]. By Lemma 2.1, for n >= 2 and a coprime to n this holds if and only if n is prime. -/ def polyFermat (n a : ℕ) : Prop := ((X + C (a : ZMod n)) ^ n : Polynomial (ZMod n)) = X ^ n + C (a : ZMod n) /-- Congruence (2) of the paper: (X + a)^n = X^n + a in Z_n[X] modulo the ideal generated by X^r - 1. Every prime n satisfies this for all a and r; the algorithm of Section 4 tests it for a single r and a range of a's. -/ def cycCong (n r a : ℕ) : Prop := (X ^ r - 1 : Polynomial (ZMod n)) ∣ (X + C (a : ZMod n)) ^ n - (X ^ n + C (a : ZMod n)) /-- Definition 4.4 of the paper: m is introspective for f if f(X)^m = f(X^m) modulo X^r - 1 over F_p. -/ def introspective (p r : ℕ) (f : Polynomial (ZMod p)) (m : ℕ) : Prop := (X ^ r - 1 : Polynomial (ZMod p)) ∣ f ^ m - f.comp (X ^ m) /-- The set P of the paper (Section 4): the multiplicative monoid generated by the polynomials X, X + 1, ..., X + l over F_p. -/ def inP (p ℓ : ℕ) (f : Polynomial (ZMod p)) : Prop := ∃ e : ℕ → ℕ, f = ∏ a ∈ Finset.range (ℓ + 1), (X + C (a : ZMod p)) ^ e a end AKS
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.