Lemma 17 — Finite Field Character Sum Weil Dispersion Domination
Provedweil_exponential_sum_ap3_pos_v2analysiscombinatoricserdos-problemsnumber-theory
For character sums in F_p where the main term exceeds the Weil square-root boundary, the net 3-AP counting density is strictly positive.
Formal statement
import Mathlib
theorem weil_exponential_sum_ap3_pos_v2 (p : ℝ) (H_card : ℝ) (hp : 100 ≤ p)
(hH_bound : 2 * Real.sqrt p * H_card < (H_card ^ 3) / p) :
0 < (H_card ^ 3) / p - 2 * Real.sqrt p * H_card := by sorry