Dickson value sum for every odd normalized parameter

Removes the residual 3 ∤ h restriction from sum_dickson_eq_cubic: for every odd k coprime to n, D_(2^k+1) and D_3 have equal sums against any function on GF(2^n), even at the odd-dimensional bad residue k ≡ 3 (mod 6).

Elementary arithmetic facts about 2 ^ k + 1

The Dickson evaluation on GF(2 ^ n) only depends on the exponent mod 2 ^ (2n) - 1

theorem KasamiCyclicAdditive.sum_dickson_kasami_eq_three {K : Type u_1} [Field K] [Fintype K] {M : Type u_2} [AddCommMonoid M] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) (f : K → M) : ∑ x : K, f (Polynomial.eval x (Polynomial.dickson 1 1 (2 ^ k + 1))) = ∑ x : K, f (Polynomial.eval x (Polynomial.dickson 1 1 3))

For every odd Kasami parameter k coprime to n, the Dickson polynomial D_(2^k+1) has the same value distribution on GF(2^n) as D_3, in the strong form of equality of sums against an arbitrary function.

This is the form consumed by the MCM phase proof, and it covers the residue k ≡ 3 (mod 6), where 9 ∣ 2^k + 1 rules out the generic Dickson permutation argument.