Elementary Frobenius-sum infrastructure

This module packages the elementary facts about the partial Frobenius sum T_k(s) = ∑ i < k, s^(2^i) used by both the Fourier and permutation proofs.

The logical hierarchy is:

• frobSum_succ gives the recurrence used by frobSum_sq_add_self;
• if frobSum k s = 0, the Artin--Schreier identity gives s^(2^k) = s;
• the shared arithmetic lemmas pow_card_two_pow and pow_two_pow_gcd from Preliminaries/Arithmetic.lean then give s^(2^gcd(k,n)) = s;
• coprimality together with s ≠ 0 forces s = 1, while oddness gives frobSum k 1 = 1, contradicting the assumed zero. The resulting frobSum_ne_zero_of_odd theorem is the public payoff.

frobSum_succ
      |
      v
frobSum_sq_add_self
      |
      |  if frobSum k s = 0
      v
s^(2^k) = s -----------\
                         \
pow_card_two_pow --------> pow_two_pow_gcd
                           |
                           v
                 s^(2^gcd(k,n)) = s
                           |
                    gcd(k,n) = 1
                           |
                           v
                        s^2 = s
                           |
                    s ≠ 0 => s = 1
                           |
frobSum_one --------------+
                           |
                           v
                     contradiction

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

T_k(s)=s+s^2+...+s^(2^(k-1)).

Equations

• KasamiCyclicAdditive.frobSum k s = ∑ i ∈ Finset.range k, s ^ 2 ^ i

theorem KasamiCyclicAdditive.frobSum_succ {K : Type u_1} [Field K] (k : ℕ) (s : K) : frobSum (k + 1) s = frobSum k s + s ^ 2 ^ k

One further term of the Frobenius sum.

theorem KasamiCyclicAdditive.frobSum_one {K : Type u_1} [Field K] [CharP K 2] {k : ℕ} (hk : Odd k) : frobSum k 1 = 1

For odd k, frobSum k 1 = 1.

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

frobSum k satisfies the Artin--Schreier identity.

theorem KasamiCyclicAdditive.frobSum_ne_zero_of_odd {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) {s : K} (hs : s ≠ 0) : frobSum k s ≠ 0

Under the odd Kasami hypotheses, frobSum k s is nonzero for s ≠ 0.