Lenstra's injectivity: distinct low-degree elements of P stay distinct in F_p[X]/(h) (Lemma 4.7)
ProvedAKS.group_injLemma 4.7 of the paper, attributed to Hendrik Lenstra Jr.: the group G-cal, generated by the images of X, X+1, ..., X+ell in the field F = F_p[X]/(h), is large - at least the binomial coefficient C(t + ell, t - 1) - because any two distinct polynomials of P of degree less than t map to distinct elements of F. The proof: if f and g of P agreed in F, then for every m of I, introspection and the agreement of the m-th powers would give f(X^m) = g(X^m) in F; the m-th powers of the primitive r-th root X range over t distinct elements indexed by the residue group G, so f(Y) - g(Y) would have t distinct roots while having degree less than t, impossible over a field.
Formalization Note The statement is the injectivity itself in the paper's form: h is an irreducible factor of X^r - 1 over F_p with no smaller power of X collapsing (h does not divide X^k - 1 for 0 < k < r), the field is AdjoinRoot h, the introspectivity of I for P and the bound t at most the size of the residue group G are hypotheses, and the conclusion is the inequality of the two images. The cardinality consequence - at least C(t + ell, t - 1) elements, by the stars-and-bars count over the exponent vectors and the unique factorization of the generator products - is part of the goal's proposed work.
import Mathlib import Definitions.Def_AKS_poly import Definitions.Def_AKS_alg
namespace AKS
/-! Lemma 4.7 of the paper (Hendrik Lenstra Jr.): distinct polynomials of P
of degree less than t map to distinct elements of the field F_p[X]/(h). -/
theorem group_inj (n p r t ℓ : ℕ) [Fact (Nat.Prime p)]
(h : Polynomial (ZMod p)) [Fact (Irreducible h)]
(hdiv : h ∣ (Polynomial.X ^ r - 1 : Polynomial (ZMod p)))
(hprim : ∀ k : ℕ, 0 < k → k < r →
¬ h ∣ (Polynomial.X ^ k - 1 : Polynomial (ZMod p)))
(hintros : ∀ m, inI n p m → ∀ f, inP p ℓ f → introspective p r f m)
(ht : t ≤ (Gfin n p r).card)
(f g : Polynomial (ZMod p)) (hf : inP p ℓ f) (hg : inP p ℓ g)
(hne : f ≠ g) (hft : Polynomial.natDegree f < t)
(hgt : Polynomial.natDegree g < t) :
Polynomial.aeval (AdjoinRoot.root h) f
≠ Polynomial.aeval (AdjoinRoot.root h) g := by sorry
end AKS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: fix n, p, r, t, ell with p prime, and an irreducible h over F_p dividing X^r - 1 and dividing no X^k - 1 for 0 < k < r; assume every m of I = {(n/p)^i p^j} is introspective for every f of P, the products of X through X + ell; assume t is at most the number of residues modulo r of I inside the window. Then two distinct polynomials f and g of P, both of degree less than t, have distinct images in the field F_p[X]/(h).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.