Reduction of the Kasami parameter modulo the extension degree

The literature statement only requires gcd(k,n)=1; it does not normalize k to the range 1 ≤ k < n. The substantive proof is naturally carried out in that range.

This file proves that the Kasami exponent, derivative image, and coefficient triple count are unchanged when k is replaced by k % n over a field of cardinality 2^n. Thus the normalization used by the proof is a theorem, not an extra hypothesis in the statement.

theorem KasamiCyclicAdditive.kasamiExponent_modEq_degree (n k : ℕ) : kasamiExponent k ≡ kasamiExponent (k % n) [MOD 2 ^ n - 1]

The Kasami exponent is periodic in k modulo n, modulo the multiplicative exponent 2^n - 1 of GF(2^n)^×.

theorem KasamiCyclicAdditive.pow_eq_of_modEq_card_sub_one {K : Type u_1} [Field K] [Fintype K] (x : K) {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a ≡ b [MOD Fintype.card K - 1]) : x ^ a = x ^ b

In a finite field, nonzero powers only depend on the exponent modulo |K| - 1. The nonzero hypotheses on the exponents handle the base 0 without a separate convention.

theorem KasamiCyclicAdditive.extension_degree_at_least_two_of_coefficients {K : Type u_1} [Field K] [Fintype K] {n : ℕ} (hcard : Fintype.card K = 2 ^ n) {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : 2 ≤ n

Two distinct nonzero coefficients provide the three distinct field elements 0, v₁, and v₂. If |K| = 2^n, this already forces n ≥ 2; characteristic two is not needed for this cardinality argument.

theorem KasamiCyclicAdditive.mod_parameter_admissible {n k : ℕ} (hn : 2 ≤ n) (hkn : k.Coprime n) : 1 ≤ k % n ∧ k % n < n ∧ (k % n).Coprime n

If n ≥ 2 and k is coprime to n, then k % n is the unique normalized representative needed by the proof: it is positive, below n, and remains coprime to n.

theorem KasamiCyclicAdditive.kasamiDerivative_mod_degree {K : Type u_1} [Field K] [Fintype K] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (b : K) : kasamiDerivative k b = kasamiDerivative (k % n) b

Over a field with 2^n elements, the normalized Kasami derivative is unchanged when the parameter is reduced modulo n.

theorem KasamiCyclicAdditive.derivativeImage_mod_degree {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) : derivativeImage k K = derivativeImage (k % n) K

The derivative image is unchanged under k ↦ k % n.

theorem KasamiCyclicAdditive.coefficientTripleCount_mod_degree {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) {v₁ v₂ : K} : coefficientTripleCount k v₁ v₂ = coefficientTripleCount (k % n) v₁ v₂

The coefficient triple count is unchanged under k ↦ k % n.