Modular iteration and source linearity of the polynomial condenser map

The induction reduces after each squaring, so the degree bound is independent of the potentially exponential exponent. Characteristic two makes each squaring additive; remaindering and evaluation preserve that additivity.

theorem Algebraic.Cutwidth.Extractor.Internal.modularFrobenius_eq_pow_modByMonic {F : Type u_1} [CommRing F] (E f : Polynomial F) (j : ℕ) : modularFrobenius E j f = f ^ 2 ^ j %ₘ E

theorem Algebraic.Cutwidth.Extractor.Internal.modularFrobenius_degree_lt {F : Type u_1} [CommRing F] [Nontrivial F] (E f : Polynomial F) (monic : E.Monic) (j : ℕ) : (modularFrobenius E j f).degree < E.degree

theorem Algebraic.Cutwidth.Extractor.Internal.modularFrobenius_zero {F : Type u_1} [CommRing F] (E : Polynomial F) (j : ℕ) : modularFrobenius E j 0 = 0

theorem Algebraic.Cutwidth.Extractor.Internal.modularFrobenius_add {F : Type u_1} [CommRing F] [CharP F 2] (E f g : Polynomial F) (j : ℕ) : modularFrobenius E j (f + g) = modularFrobenius E j f + modularFrobenius E j g

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialCondenser_apply {F : Type u_1} [CommRing F] (E f : Polynomial F) (r m : ℕ) (y : F) (i : Fin m) : polynomialCondenser E r m f y i = Polynomial.eval y (f ^ (2 ^ r) ^ ↑i %ₘ E)

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialCondenser_zero_coordinate {F : Type u_1} [CommRing F] [Nontrivial F] (E f : Polynomial F) (monic : E.Monic) (source : f.degree < E.degree) (r m : ℕ) (y : F) : polynomialCondenser E r (m + 1) f y 0 = Polynomial.eval y f

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialCondenser_zero {F : Type u_1} [CommRing F] (E : Polynomial F) (r m : ℕ) (y : F) : polynomialCondenser E r m 0 y = 0

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialCondenser_add {F : Type u_1} [CommRing F] [CharP F 2] (E f g : Polynomial F) (r m : ℕ) (y : F) : polynomialCondenser E r m (f + g) y = polynomialCondenser E r m f y + polynomialCondenser E r m g y

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialCondenser_smul {F : Type u_1} [CommRing F] [CharP F 2] [Module (ZMod 2) F] (E f : Polynomial F) (r m : ℕ) (y : F) (c : ZMod 2) : polynomialCondenser E r m (c • f) y = c • polynomialCondenser E r m f y