Equal-degree factors in a successful auxiliary root lift

theorem MIPRE.LowDegree.BinaryPolynomial.comp_dvd_card_sub_one_of_residue {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Fintype K] (f : Polynomial F) (hi : Irreducible f) (a b : K) (ha : (Polynomial.aeval a) f = 0) (ha0 : a ≠ 0) (q : ℕ) (hq : q ∣ Fintype.card K - 1) (hb : b ^ q = a) : f.comp (Polynomial.X ^ q) ∣ Polynomial.X ^ (Fintype.card K - 1) - 1

A residue root forces the substituted polynomial to divide the multiplicative field polynomial. This exponentially large polynomial is only a proof device.

theorem MIPRE.LowDegree.BinaryPolynomial.natDegree_le_of_dvd_comp_power {F : Type u_1} [Field F] (f g : Polynomial F) (hf : f.Monic) (hi : Irreducible f) (hg : Irreducible g) (q : ℕ) (hd : g ∣ f.comp (Polynomial.X ^ q)) : f.natDegree ≤ g.natDegree

A factor of a power substitution has at least the original irreducible degree.

theorem MIPRE.LowDegree.BinaryPolynomial.residue_factor_natDegree {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] [Fintype K] (f g : Polynomial F) (hf : f.Monic) (hi : Irreducible f) (hg : Irreducible g) (hcard : Fintype.card K = Nat.card F ^ f.natDegree) (a b : K) (ha : (Polynomial.aeval a) f = 0) (ha0 : a ≠ 0) (q : ℕ) (hq : q ∣ Fintype.card K - 1) (hb : b ^ q = a) (hd : g ∣ f.comp (Polynomial.X ^ q)) : g.natDegree = f.natDegree

Every irreducible factor in a residue lift has exactly the old degree.