# The optimal order of convex-body covering density

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A single-lattice covering bound of order $n\log n$](../../preprints/A-single-lattice-covering-bound-of-order-n-log-n-September-23-2026/paper.pdf)
- [Translative covering densities of order $n\log n$](../../preprints/Translative-covering-densities-of-order-n-log-n-September-23-2026/paper.pdf)

## Scope

The formalized result gives an absolute constant $C>0$ such that every convex body $K\subset\mathbb R^n$, $n\ge2$, admits a covering by translates along one full-rank lattice $L$ with density $|K|/\mathrm{covol}(L)\le Cn\log n$. The covering is exact, and no symmetry, boundary regularity, or volume normalization is assumed.

The formalization determines the order of the largest covering density in dimension $n$. For all sufficiently large $n$, the suprema of translative covering density and lattice covering density are each bounded above and below by absolute positive multiples of $n\log n$, both over all convex bodies and over centrally symmetric convex bodies.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Single-lattice covering bound | [SingleLatticeCovering.lean](../ComparatorChallenges/SingleLatticeCovering.lean) |
| Optimal order for translative and lattice covering-density suprema | [CoveringDensity.lean](../ComparatorChallenges/CoveringDensity.lean) |