Erdős-Ginzburg-Ziv Theorem on Zero-Sum Sequences

This preprint provides an exhaustive mathematical treatise on the Erdős-Ginzburg-Ziv (EGZ) Theorem (Problem #06 in Paul Erdős' collection, 1961), a foundational pillar of additive number theory, finite abelian group theory, and zero-sum Ramsey combinatorics. The theorem asserts that every sequence of 2n − 1 integers contains a subsequence of length exactly n whose sum is divisible by n: ∀ a1, …, a2n−1 ∈ ℤ, ∃ I ⊆ {1, …, 2n−1}, |I| = n and ∑ i ∈ I ai ≡ 0 &pmod; n The length threshold 2n − 1 is strictly sharp, as evidenced by the extremal counter-example of n − 1 zeros and n − 1 ones. This treatise establishes the algebraic mechanisms connecting EGZ with the Davenport constant D(G), finite field nullstellensatz methods, and multi-dimensional lattice generalizations. Key Mathematical Results & Contributions Proof for Prime Moduli via Chevalley-Warning: Rigorous polynomial derivation over the finite field 𝔽p using the system of degree p − 1 symmetric power equations and Cauchy-Davenport additive expansion. Complete Composite Induction: Non-elliptical proof demonstrating that if EGZ holds for integers a and b, it holds unconditionally for their product n = ab by block partitioning and hierarchical averaging. Exact Sharpness & Extremal Multisets: Proof that the multiset {0n−1, 1n−1} admits no n-element zero-sum subset modulo n, strictly establishing the minimality of 2n − 1. Lattice Generalizations & Kemnitz's Conjecture: Review of Christian Reiher's theorem (2007) on two-dimensional integer lattices ℤp2 proving s(ℤ p2) = 4p − 3. 100% Machine-Checked Verification in Lean 4: Base cases (n = 1 and n = 2 via pigeonhole parity), sharpness bounds, and submultiset sum predicates are machine-certified with 0 axioms, 0 linter warnings, and 0 sorry placeholders via the Lean 4 interactive theorem prover and Mathlib. Repository and Verification Artifacts The companion machine-checked code and formal verification artifacts are publicly hosted on GitHub:https://github.com/flouzzy/erdos-problemsInteractive Portal: https://maths-proofs.edounze.com/#erdos-06-ginzburg-ziv Primary MSC (2020): 11B75, 11P70, 05D10, 68V20, 20K01.Keywords: Erdős-Ginzburg-Ziv Theorem, Zero-Sum Sequences, Davenport Constant, Chevalley-Warning Theorem, Cauchy-Davenport Theorem, Kemnitz's Conjecture, Formal Verification, Lean 4, Mathlib.