The MCM permutation theorem

The Muller--Cohen--Matthews permutation theorem is proved here rather than imported. The ingredients are

• mcmCharSum_eq_dickson for generic multiplicative characters;
• cubic_mcm_apply for the exceptional cubic characters;
• dickson_bijective for the required Dickson permutation;
• bijective_of_mulChar_sum_eq for the final permutation argument.

The key character-sum theorem says that every nonprincipal multiplicative character has vanishing untwisted MCM sum. Together with the elementary fact that the MCM map has zero as its unique zero, this makes all multiplicative character sums preserved, hence the MCM map a permutation.

theorem KasamiCyclicAdditive.odd_coprime_two_mul {k n : ℕ} (hk : Odd k) (hkn : k.Coprime n) : k.Coprime (2 * n)

Odd k coprime to n is also coprime to 2n.

The MCM map has no nonzero zero

theorem KasamiCyclicAdditive.mcmMap_ne_zero_of_ne_zero {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) {s : K} (hs : s ≠ 0) : mcmMap k s ≠ 0

Under the odd Kasami hypotheses, mcmMap k maps nonzero elements to nonzero elements.

theorem KasamiCyclicAdditive.mcmMap_eq_zero_iff {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) (s : K) : mcmMap k s = 0 ↔ s = 0

Zero is the unique zero of the odd-parameter MCM map.

Character sums

theorem KasamiCyclicAdditive.mcmCharSum_eq_zero_of_ne_one {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hklt : k < n) (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) (χ : MulChar K ℂ) (hchi : χ ≠ 1) : mcmCharSum k χ = 0

Every nonprincipal multiplicative character has vanishing untwisted MCM sum under the odd Kasami hypotheses.

theorem KasamiCyclicAdditive.mcmCharSum_eq_sum_of_odd {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hklt : k < n) (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) (χ : MulChar K ℂ) : mcmCharSum k χ = ∑ s : K, χ s

Every multiplicative character sum is preserved by the odd-parameter MCM map. The nonprincipal case is mcmCharSum_eq_zero_of_ne_one; the principal case uses that zero is the unique zero.

theorem KasamiCyclicAdditive.mcmMap_bijective_of_odd {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hklt : k < n) (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) : Function.Bijective (mcmMap k)

Muller--Cohen--Matthews permutation theorem. For odd k < n coprime to n, the MCM map is a permutation of every characteristic two finite field of order 2^n.