Introspective numbers

Fix a prime p, a number r, and a field K that is an algebra over ℤ / p. A number m is introspective for a polynomial f over ℤ / p if f(η)^m = f(η^m) for every r-th root of unity η of K (Cslib.AKS.Introspective). This is the form of Agrawal, Kayal and Saxena's introspection f(X)^m ≡ f(X^m) (mod X^r - 1, p) that their proof uses, evaluated at roots of unity as in Lenstra's exposition Agrawal, Kayal, Saxena, Section 4.

• p is introspective for every f, by the Frobenius map (introspective_prime).
• Introspective numbers are closed under products, and introspective polynomials under products (Introspective.mul, Introspective.mul_poly).
• If p ∣ n and the AKS congruence (X + a)^n ≡ X^n + a (mod X^r - 1, n) holds, then n is introspective for X + a (introspective_of_congruence).
• If n is introspective for f and p ∣ n, so is n / p, because the Frobenius map of a field of characteristic p is injective (Introspective.div_prime).

Main definitions

• Cslib.AKS.Introspective: f(η)^m = f(η^m) at every r-th root of unity η.

Main results

• Cslib.AKS.introspective_prime, Cslib.AKS.introspective_of_congruence, Cslib.AKS.Introspective.div_prime: the basic introspective numbers.
• Cslib.AKS.Introspective.mul, Cslib.AKS.Introspective.mul_poly, Cslib.AKS.Introspective.multiset_prod: closure properties.

References

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

def Cslib.AKS.Introspective {p : ℕ} (K : Type u_1) [Field K] [Algebra (ZMod p) K] (r m : ℕ) (f : Polynomial (ZMod p)) : Prop

m is introspective for f (with respect to r): f(η)^m = f(η^m) for every r-th root of unity η of K.

theorem Cslib.AKS.introspective_prime {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] [Fact (Nat.Prime p)] (r : ℕ) (f : Polynomial (ZMod p)) : Introspective K r p f

The prime is introspective for every polynomial: f(η)^p = f(η^p) by the Frobenius map, since the coefficients of f lie in ℤ / p.

theorem Cslib.AKS.Introspective.mul {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] {r m m' : ℕ} {f : Polynomial (ZMod p)} (hm : Introspective K r m f) (hm' : Introspective K r m' f) : Introspective K r (m * m') f

Introspective numbers are closed under products.

theorem Cslib.AKS.Introspective.mul_poly {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] {r m : ℕ} {f g : Polynomial (ZMod p)} (hf : Introspective K r m f) (hg : Introspective K r m g) : Introspective K r m (f * g)

Introspective polynomials are closed under products.

theorem Cslib.AKS.introspective_one {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] (r m : ℕ) : Introspective K r m 1

Every number is introspective for the constant 1.

theorem Cslib.AKS.introspective_X {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] (r m : ℕ) : Introspective K r m Polynomial.X

Every number is introspective for X.

theorem Cslib.AKS.Introspective.multiset_prod {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] {r m : ℕ} {s : Multiset (Polynomial (ZMod p))} (hs : ∀ f ∈ s, Introspective K r m f) : Introspective K r m s.prod

Products of introspective polynomials are introspective.

theorem Cslib.AKS.Introspective.pow {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] {r m : ℕ} {f : Polynomial (ZMod p)} (hm : Introspective K r m f) (k : ℕ) : Introspective K r (m ^ k) f

Every power of m is introspective when m is.

theorem Cslib.AKS.introspective_of_congruence {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] {r n a : ℕ} (hpn : p ∣ n) (h : Congruence n r a) : Introspective K r n (Polynomial.X + Polynomial.C ↑a)

The AKS congruence gives introspection. If p ∣ n and (X + a)^n ≡ X^n + a (mod X^r - 1, n), then n is introspective for X + a.

theorem Cslib.AKS.Introspective.div_prime {p : ℕ} {K : Type u_1} [Field K] [Algebra (ZMod p) K] {r : ℕ} {f : Polynomial (ZMod p)} [Fact (Nat.Prime p)] {n : ℕ} (hpn : p ∣ n) (hn : Introspective K r n f) : Introspective K r (n / p) f

n / p is introspective when n is, for p ∣ n: both (f(η)^{n/p})^p and f(η^{n/p})^p equal f(η^n), and the Frobenius map of K is injective.