Algebraic progress and stopping criteria for auxiliary root lifting

theorem MIPRE.LowDegree.BinaryPolynomial.primitiveRoot_of_prime_power_root {M : Type u_1} [CommMonoid M] (x : M) (q s : ℕ) (hq : Nat.Prime q) (hs : 0 < s) (hx : IsPrimitiveRoot (x ^ q) (q ^ s)) : IsPrimitiveRoot x (q ^ (s + 1))

Extracting one more prime root increases its prime-power order by exactly one power.

theorem MIPRE.LowDegree.BinaryPolynomial.aeval_ne_zero_of_finrank_lt {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] (g : Polynomial F) (hg : g.Monic) (hi : Irreducible g) (hd : Module.finrank F K < g.natDegree) (x : K) : (Polynomial.aeval x) g ≠ 0

An irreducible monic polynomial cannot have a root in a smaller-dimensional extension.

theorem MIPRE.LowDegree.BinaryPolynomial.nonresidue_of_irreducible_comp {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] (f : Polynomial F) (hf : f.Monic) (hd : Module.finrank F K = f.natDegree) (hp : 0 < f.natDegree) (q : ℕ) (hq : 1 < q) (a : K) (ha : (Polynomial.aeval a) f = 0) (hi : Irreducible (f.comp (Polynomial.X ^ q))) (b : K) : b ^ q ≠ a

Irreducibility of the substituted polynomial certifies a nonresidue at the old root. This is the soundness of the executable singleton-factor stopping test.