Half-size of the Kasami derivative image

For odd k, mcmMap k is globally bijective, hence injective on the Artin--Schreier image. Since

derivativeImage k K = image (mcmMap k) (asSet K)

and asSet has exactly half the elements of K, the derivative image has half the field. For even k, coprimality forces n - k to be odd, and the Frobenius transport of MCM/ComplementTransport.lean preserves the cardinality of the derivative image.

theorem KasamiCyclicAdditive.kasami_half_size_odd {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k : ℕ} (hklt : k < n) (hcard : Fintype.card K = 2 ^ n) (hkodd : Odd k) (hkn : k.Coprime n) : 2 * (derivativeImage k K).card = Fintype.card K

For odd k, the Kasami normalized derivative image has exactly half the field, as a direct consequence of the MCM permutation theorem.

theorem KasamiCyclicAdditive.odd_complement_of_even_coprime {n k : ℕ} (hklt : k < n) (hkn : k.Coprime n) (hke : Even k) : Odd (n - k)

With gcd (k, n) = 1 and k even, the complementary parameter n - k is odd.

theorem KasamiCyclicAdditive.kasami_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k : ℕ} (hkpos : 1 ≤ k) (hklt : k < n) (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) : 2 * (derivativeImage k K).card = Fintype.card K

For every admissible k, the Kasami normalized derivative image has exactly half the field. Odd k is the MCM theorem; even k is transported to the odd complementary parameter n-k.