Arithmetic for the exceptional MCM character case

For coprime k,n, every common divisor of 2^k+1 and 2^n-1 divides 3. Thus a multiplicative character on GF(2^n) killed by 2^k+1 is automatically cubic. This is the exceptional branch complementary to the generic Dickson permutation argument.

theorem KasamiCyclicAdditive.gcd_two_mul_dvd_two {k n : ℕ} (hkn : k.Coprime n) : (2 * k).gcd n ∣ 2

If gcd(k,n)=1, then gcd(2k,n) divides 2.

theorem KasamiCyclicAdditive.dvd_three_of_dvd_two_pow_add_one_two_pow_sub_one {d k n : ℕ} (hkn : k.Coprime n) (hplus : d ∣ 2 ^ k + 1) (hminus : d ∣ 2 ^ n - 1) : d ∣ 3

A common divisor of 2^k+1 and 2^n-1, with gcd(k,n)=1, divides 3.

theorem KasamiCyclicAdditive.mulChar_cube_eq_one_of_kasami_exceptional {K : Type u_1} [Field K] [Fintype K] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (hkn : k.Coprime n) (χ : MulChar K ℂ) (he : χ ^ (2 ^ k + 1) = 1) : χ ^ 3 = 1

On a field of order 2^n, a character satisfying χ^(2^k+1)=1 is cubic whenever gcd(k,n)=1.