Combinatorial core of κ(F_q(x)) = ω²

The combinatorial core of the lower bound κ(F_q(x)) = ω² for the length of the DGH stratification.

Let L be a prime, G an additive commutative group, and f : ℤ → G an L-periodic function that is a finite sum of k arithmetic-progression indicators, f n = ∑ i, [n ≡ m i (mod N i)] • c i. Then f is constant on all residues mod L except at most k of them.

Proof sketch

• M := ∏_{i : L ∤ N i} N i is coprime to L; pick b with b·M ≡ 1 (mod L).
• For r : ℤ, n := b·M·r ≡ r (mod L), so f r = f n. Terms with L ∤ N i are evaluated at a multiple of N i, hence equal the constant c₀. So f r ≠ c₀ forces some i with L ∣ N i.
• Such an i determines r mod L, so the bad residues inject into Fin k.

The hypotheses k < L and N i ≥ 1 are not needed.

Main results

• card_ne_const_le, card_ne_const_le_of_lt.

theorem DGH.FqLower.card_ne_const_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (L : ℕ) (hL : Nat.Prime L) (k : ℕ) (N : Fin k → ℕ) (m : Fin k → ℤ) (c : Fin k → G) (f : ℤ → G) (hper : ∀ (n : ℤ), f (n + ↑L) = f n) (hf : ∀ (n : ℤ), f n = ∑ i : Fin k, if n ≡ m i [ZMOD ↑(N i)] then c i else 0) : ∃ (c₀ : G), {r ∈ Finset.range L | f ↑r ≠ c₀}.card ≤ k

Core counting lemma (no k < L, no N i ≥ 1 needed).

theorem DGH.FqLower.card_ne_const_le_of_lt {G : Type u_1} [AddCommGroup G] [DecidableEq G] (L : ℕ) (hL : Nat.Prime L) (k : ℕ) (_hk : k < L) (N : Fin k → ℕ) (_hN : ∀ (i : Fin k), 1 ≤ N i) (m : Fin k → ℤ) (c : Fin k → G) (f : ℤ → G) (hper : ∀ (n : ℤ), f (n + ↑L) = f n) (hf : ∀ (n : ℤ), f n = ∑ i : Fin k, if n ≡ m i [ZMOD ↑(N i)] then c i else 0) : ∃ (c₀ : G), {r ∈ Finset.range L | f ↑r ≠ c₀}.card ≤ k

The statement in the form requested (with the unused hypotheses k < L, 1 ≤ N i).