OAI/Geometry/LatticeCovering/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform, unconditional single-lattice covering bound in every dimension at least two. The eventual bound uses the proved analytic and geometric producers; finite-dimensional absorption supplies one absolute constant for all dimensions.

  1. theorem OAI.SingleLatticeCovering.single_lattice_covering line 25

    Distinct definitions of this name: ComparatorChallenges/SingleLatticeCovering.lean:20 (same statement text; different proof or body). Qualify references as OAI.SingleLatticeCovering.single_lattice_covering@path.