The MCM/Dickson phase formula

Proves the Dillon--Kashyap phase formula DillonKashyapPhaseFormula directly from the derivative-image half-size equation plus the MCM/Dickson identities — no Dillon--Kashyap or Dillon--Dobbertin Fourier theorem is imported.

theorem KasamiCyclicAdditive.eq_one_of_pow_eq_one_of_coprime_order_dvd {G : Type u_2} [Monoid G] {x : G} {a N : ℕ} (hcop : a.Coprime N) (hpow : x ^ a = 1) (hord : orderOf x ∣ N) : x = 1

A coprime power relation and an order divisibility bound force the element to be one.

theorem KasamiCyclicAdditive.mcmTwistedCharSum_eq_gaussSum_mul_gaussSum_div_gaussSum_of_generic {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) {chi : MulChar K ℂ} (hchie : chi ^ (2 ^ k + 1) ≠ 1) (hchi3 : chi ^ 3 ≠ 1) : mcmTwistedCharSum k (primitiveAddChar K) chi = gaussSum chi (primitiveAddChar K) * gaussSum (chi ^ (2 ^ k + 1)) (primitiveAddChar K) / gaussSum (chi ^ 3) (primitiveAddChar K)

The generic twisted MCM sum factors into three Gauss sums.

theorem KasamiCyclicAdditive.phase_formula_from_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k m : ℕ} (hklt : k < n) (hk : Odd k) (hcard : Fintype.card K = 2 ^ n) (hkn : k.Coprime n) (he : 2 ^ k + 1 = 3 * m) (hcop : m.Coprime (2 ^ n - 1)) (hhalf : 2 * (derivativeImage k K).card = Fintype.card K) : DillonKashyapPhaseFormula k (primitiveAddChar K)

Phase formula. The Dillon--Kashyap phase formula follows from the half-size packet plus the MCM/Dickson identities; no Dillon--Kashyap or Dillon--Dobbertin Fourier theorem is imported.

he and hcop are the normalized arithmetic data. They are what shows chi^(2^k+1) ≠ 1 for every character outside the principal and cubic exceptional cases.