The MCM half-space packet

Derives the Muller--Cohen--Matthews parametrization of the Kasami derivative image Δ algebraically, then uses the derivative-image half-size equation to convert sums over the image into Artin--Schreier half-space sums. No APN or two-to-one theorem for the Kasami derivative is imported.

Writing A(b) = b² + b for the Artin--Schreier map, T_k(s) = ∑_{i<k} s^(2^i) and M_k(s) = T_k(s)^(2^k+1) / s^(2^k) for the MCM map, the main identities are

• δ(b) = M_k(A(b)), so Δ is the image of the Artin--Schreier image under M_k;
• the Artin--Schreier image is exactly the kernel of the canonical trace character, and has half the elements of K;
• consequently sums over Δ are half-space sums weighted by 1 + ψ(s).

def KasamiCyclicAdditive.artinSchreier {K : Type u_1} [Field K] (b : K) : K

Artin--Schreier map in characteristic two.

Equations

• KasamiCyclicAdditive.artinSchreier b = b ^ 2 + b

def KasamiCyclicAdditive.asSet (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] : Finset K

Artin--Schreier image.

Equations

• KasamiCyclicAdditive.asSet K = Finset.image KasamiCyclicAdditive.artinSchreier Finset.univ

def KasamiCyclicAdditive.mcmMap {K : Type u_1} [Field K] (k : ℕ) (s : K) : K

MCM map, with Lean's field convention making M_k(0)=0.

Equations

• KasamiCyclicAdditive.mcmMap k s = KasamiCyclicAdditive.frobSum k s ^ (2 ^ k + 1) / s ^ 2 ^ k

Traces of finite fields are Frobenius invariant

theorem KasamiCyclicAdditive.trace_pow_natCard {F : Type u_2} {L : Type u_3} [Field F] [Field L] [Finite L] [Algebra F L] (x : L) : (Algebra.trace F L) (x ^ Nat.card F) = (Algebra.trace F L) x

The trace of a finite extension is invariant under the #F-power Frobenius.

theorem KasamiCyclicAdditive.primitiveAddChar_sq {K : Type u_1} [Field K] [Fintype K] [CharP K 2] (x : K) : (primitiveAddChar K) (x ^ 2) = (primitiveAddChar K) x

In characteristic two the canonical trace character is invariant under squaring.

The algebraic MCM identity

theorem KasamiCyclicAdditive.frobSum_artinSchreier {K : Type u_1} [Field K] [CharP K 2] (k : ℕ) (b : K) : frobSum k (artinSchreier b) = b ^ 2 ^ k + b

The Artin--Schreier map telescopes the Frobenius sum.

theorem KasamiCyclicAdditive.kasamiDerivative_mul_artinSchreier_pow {K : Type u_1} [Field K] [CharP K 2] (k : ℕ) (b : K) : kasamiDerivative k b * artinSchreier b ^ 2 ^ k = frobSum k (artinSchreier b) ^ (2 ^ k + 1)

The cleared-denominator form of the MCM identity.

theorem KasamiCyclicAdditive.kasamiDerivative_eq_mcmMap {K : Type u_1} [Field K] [CharP K 2] (k : ℕ) (b : K) : kasamiDerivative k b = mcmMap k (artinSchreier b)

The algebraic MCM identity. This includes the b=0,1 denominator cases; no nonzero hypothesis on b^2+b is assumed.

The half-space sum

theorem KasamiCyclicAdditive.artinSchreier_eq_iff {K : Type u_1} [Field K] [CharP K 2] (a b : K) : artinSchreier a = artinSchreier b ↔ a = b ∨ a = b + 1

The Artin--Schreier map is exactly two-to-one.

theorem KasamiCyclicAdditive.card_asSet {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] : 2 * (asSet K).card = Fintype.card K

The Artin--Schreier image has exactly half of the elements of K.

theorem KasamiCyclicAdditive.primitiveAddChar_artinSchreier {K : Type u_1} [Field K] [Fintype K] [CharP K 2] (b : K) : (primitiveAddChar K) (artinSchreier b) = 1

The Artin--Schreier image lies in the kernel of the trace character.

theorem KasamiCyclicAdditive.asSet_eq_kernel {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] : asSet K = {s : K | (primitiveAddChar K) s = 1}

Artin--Schreier trace-zero criterion: the Artin--Schreier image is exactly the kernel of the trace character.

theorem KasamiCyclicAdditive.derivativeImage_eq_image {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (k : ℕ) : derivativeImage k K = Finset.image (mcmMap k) (asSet K)

The derivative image is the image of the Artin--Schreier image under the MCM map.

theorem KasamiCyclicAdditive.mcm_halfspace_sum {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {k : ℕ} (hhalf : 2 * (derivativeImage k K).card = Fintype.card K) (f : K → ℂ) : 2 * ∑ t ∈ derivativeImage k K, f t = ∑ s : K, (1 + (primitiveAddChar K) s) * f (mcmMap k s)

The MCM half-space identity, in the form consumed by the Fourier argument.

hhalf is the half-size fact for the derivative image, and it is enough: kasamiDerivative_eq_mcmMap gives a surjection asSet → derivativeImage, the Artin--Schreier map has two-element fibers, so |asSet| = |K|/2, and the two equal-size sets are therefore in bijection under mcmMap. Moreover asSet is exactly the kernel of primitiveAddChar, and every value of an additive character on a characteristic-two group squares to 1, so the weight 1 + ψ(s) is 2 on asSet and 0 off it.