Primitive-root progress and squarefreeness in auxiliary lifting

theorem MIPRE.LowDegree.BinaryPolynomial.oddPrimePower_cast_ne_zero (q s : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : ↑(q ^ s) ≠ 0

Odd prime powers remain nonzero over the binary field.

theorem MIPRE.LowDegree.BinaryPolynomial.primitiveRoot_of_aeval_dvd_cyclotomic {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (f : Polynomial F) (n : ℕ) [NeZero ↑n] (hd : f ∣ Polynomial.cyclotomic n F) (z : K) (hz : (Polynomial.aeval z) f = 0) : IsPrimitiveRoot z n

Any root of a cyclotomic divisor has the prescribed primitive order.

theorem MIPRE.LowDegree.BinaryPolynomial.lifted_root_primitive (f g : Polynomial (ZMod 2)) (q s : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hs : 0 < s) (hg : Irreducible g) (hf : f ∣ Polynomial.cyclotomic (q ^ s) (ZMod 2)) (hd : g ∣ f.comp (Polynomial.X ^ q)) : IsPrimitiveRoot (AdjoinRoot.root g) (q ^ (s + 1))

Each factor chosen in a lift advances primitive prime-power order.

theorem MIPRE.LowDegree.BinaryPolynomial.lifted_factor_dvd_cyclotomic (f g : Polynomial (ZMod 2)) (q s : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hs : 0 < s) (hg : Irreducible g) (hf : f ∣ Polynomial.cyclotomic (q ^ s) (ZMod 2)) (hd : g ∣ f.comp (Polynomial.X ^ q)) : g ∣ Polynomial.cyclotomic (q ^ (s + 1)) (ZMod 2)

The cyclotomic divisibility invariant passes to every chosen factor.

theorem MIPRE.LowDegree.BinaryPolynomial.squarefree_comp_power_of_dvd_cyclotomic (f : Polynomial (ZMod 2)) (q s : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hf : f ∣ Polynomial.cyclotomic (q ^ s) (ZMod 2)) : Squarefree (f.comp (Polynomial.X ^ q))

Every substitution queried by the auxiliary loop is squarefree.