The polynomial Fermat characterization of the primes (Lemma 2.1)
ProvedAKS.poly_fermatLemma 2.1 of Agrawal, Kayal, and Saxena's paper (Annals of Mathematics 160 (2004) 781-793): the generalization of Fermat's Little Theorem to polynomial rings. For n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in the polynomial ring over Z_n. The forward direction is the freshman's dream in Z_p[X] - every binomial coefficient C(p, i) with 0 < i < p is divisible by p - together with Fermat's little theorem for the base a. The backward direction isolates the coefficient of X^q, for a prime q with q^k dividing n exactly: the coefficient is C(n, q) a^(n-q), whose q-adic valuation falls below k because q^k does not divide C(n, q) and q does not divide a, so the identity fails in Z_n[X].
Formalization Note The congruence is stated as the definition polyFermat n a, an equality in Polynomial (ZMod n); the coprimality of a and n is a hypothesis, as in the paper.
import Mathlib import Definitions.Def_AKS_poly import Definitions.Def_AKS_alg
namespace AKS
/-! Lemma 2.1 of the paper: the polynomial Fermat characterization of the
primes. -/
theorem poly_fermat (n a : ℕ) (hn : 2 ≤ n) (ha : Nat.gcd a n = 1) :
Nat.Prime n ↔ polyFermat n a := by sorry
end AKS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for n at least 2 and a with gcd(a, n) = 1, n is prime exactly when the polynomial (X + a)^n equals X^n + a in Z_n[X]. No other hypotheses appear. The forward direction rests on the divisibility of the intermediate binomial coefficients by the prime; the backward direction on the nonvanishing of the coefficient of X^q modulo n for a prime q dividing n with multiplicity k, driven by q^k not dividing C(n, q) and by the coprimality of a with n.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.