Monomials on lines of a finite field

Over a finite field K with q elements, the values of a polynomial of degree below q - 1 sum to zero (FiniteField.sum_eval_eq_zero_of_natDegree_lt). The restriction of a monomial ∏ i, X i ^ e i to an affine line can have degree up to ∑ i, e i, but in characteristic two a Frobenius twist lowers it. For q = 2 ^ (r + s), substitute x = y ^ 2 ^ r and split e = e % 2 ^ s + 2 ^ s * (e / 2 ^ s); since y ^ q = y, the restriction becomes a polynomial in y of degree at most ∑ i, (2 ^ r * (e i % 2 ^ s) + e i / 2 ^ s); for e i < q this is the total of the (r + s)-digit binary exponents rotated cyclically by s digits. When it is below q - 1 the line sum vanishes (sum_prod_add_mul_pow_eq_zero). No form of Lucas's theorem is used.

Main results

• Cslib.LineCode.HighRate.sum_prod_add_mul_pow_eq_zero: monomials with small rotated degree sum to zero on every affine line.

References

• Adapted from MassProduction/HighRate/LineParity.lean, MassProduction/HighRate/PolynomialSupport.lean and MassProduction/LowDegree.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.LineCode.HighRate.sum_prod_add_mul_pow_eq_zero {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {ι : Type u_2} [Fintype ι] {r s : ℕ} (hK : Fintype.card K = 2 ^ (r + s)) (u v : ι → K) (e : ι → ℕ) (he : ∑ i : ι, (2 ^ r * (e i % 2 ^ s) + e i / 2 ^ s) < Fintype.card K - 1) : ∑ x : K, ∏ i : ι, (u i + x * v i) ^ e i = 0

Frobenius twist. Let K have 2 ^ (r + s) elements. If the exponents e i, rotated by s binary digits, have total ∑ i, (2 ^ r * (e i % 2 ^ s) + e i / 2 ^ s) below Fintype.card K - 1, then the values of the monomial ∏ i, X i ^ e i on the affine line x ↦ u + x • v sum to zero.