Polynomial support after Frobenius powers

In characteristic two, every exponent appearing in a 2^r-th power is divisible by 2^r. Multiplication by a low-degree polynomial therefore leaves the residue of each supported exponent bounded by that low degree.

theorem Algebraic.MassProduction.HighRate.dvdOfMemSupportPowTwo {K : Type u_1} [Field K] [CharP K 2] (polynomial : Polynomial K) (width exponent : ℕ) (inSupport : exponent ∈ (polynomial ^ 2 ^ width).support) : 2 ^ width ∣ exponent

Frobenius powers have support only at multiples of the power.

theorem Algebraic.MassProduction.HighRate.residueLeNatDegreeOfMemSupportMulPowTwo {K : Type u_1} [Field K] [CharP K 2] (low high : Polynomial K) (width exponent : ℕ) (inSupport : exponent ∈ (low * high ^ 2 ^ width).support) : exponent % 2 ^ width ≤ low.natDegree

A low-degree factor bounds the residue of every supported exponent after multiplication by a Frobenius power.