Introspective numbers and polynomials are closed under multiplication (Lemmas 4.5 and 4.6)
ProvedAKS.introspective_closureLemmas 4.5 and 4.6 of the paper. Introspection, the relation of Definition 4.4 - m is introspective for f when f^m = f(X^m) modulo X^r - 1 over F_p - is closed under the two multiplications that matter for the correctness proof. Lemma 4.5: if m and m' are introspective for f, then so is m m', because f^(m m') = f(X^m)^(m') = f(X^(m m')) modulo X^r - 1, using that X^r - 1 divides X^(m r) - 1. Lemma 4.6: if m is introspective for f and for g, then it is introspective for f g, because (f g)^m = f^m g^m = f(X^m) g(X^m) modulo X^r - 1. Together they imply that every number of the set I = {(n/p)^i p^j} is introspective for every polynomial of the set P of products of X, X+1, ..., X+ell.
Formalization Note The two closures are stated as one conjunction over the definition introspective p r f m; the paper's consequence - I is introspective for P - is the goal's work, via the congruences (3), (4), and (5).
import Mathlib import Definitions.Def_AKS_poly import Definitions.Def_AKS_alg
namespace AKS
/-! Lemmas 4.5 and 4.6 of the paper: introspection is closed under
multiplication of numbers and of polynomials. -/
theorem introspective_closure (p r : ℕ)
(f g : Polynomial (ZMod p)) (m m' : ℕ)
(hm : introspective p r f m) (hm' : introspective p r f m')
(hgm : introspective p r g m) :
introspective p r f (m * m') ∧ introspective p r (f * g) m := by sorry
end AKS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: over Z_p[X], with introspectivity defined relative to a modulus r: if m and m' are introspective for f, then m * m' is introspective for f; and if m is introspective for both f and g, then m is introspective for f * g. No hypotheses beyond p and r being fixed.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.