A finite set of lattice points gives disjoint translates of a fundamental domain. A bounded basis therefore gives an explicit finite-radius volume bound, without an asymptotic onset depending on the lattice.

theorem CCDN.superlattice_finite_packing_polynomial {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] [FiniteDimensional ℝ E] (b : Module.Basis ι ℝ E) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (hb : ∀ (i : ι), b i ∈ L) (s : Finset ↥L) {B M : ℝ} (hB : 0 ≤ B) (hM : 0 ≤ M) (hs : ∀ x ∈ s, ‖↑x‖ ≤ B) (hnorm : ∀ (i : ι), ‖b i‖ ≤ M) : ↑s.card * ZLattice.covolume L MeasureTheory.volume ≤ (2 * B + ↑(Fintype.card ι) * M) ^ Module.finrank ℝ E * MeasureTheory.volume.real (Metric.ball 0 1)

Polynomial-radius form of the finite packing estimate. The constant is explicit and depends only on the dimension and on the basis bound.