Convex geometry and the Erdős--Ginzburg--Ziv problem

This is the root module of the formalization project. Importing it exposes the statement of Theorem 1.2, the foundational zero-sum API, and the polynomial-method bound on the hollow constant used in the asymptotics.

The default target also checks the public convex-flag, decomposition, and downstream-consistency interfaces. The one-dimensional result remains available as EGZ.ZeroSum.DimensionOne, but is intentionally not part of the default build surface.