Lemma 12 ([Determinant-minimizing sublattice]). Let L be a lattice and let T>0 . The quantity M T^M , M⊂L a sublattice, has a minimum, attained by a primitive sublattice L₀ . It satisfies L_0≤T^L₀ , M≥T^M every sublattice M⊂L/L_0. If …

The rank-zero lattice has normalized determinant one. For a fixed positive rank t , the determinant of a sublattice is the norm of the wedge of one of its bases in the discrete lattice ^t L . There are only finitely many such norms at most T^t . Thus among all normalized determinants no greater than one there are only finitely many values, and the minimum is attained. Saturating a minimizer can only decrease its determinant while preserving its rank, so a primitive minimizer may be chosen. Comparison with the rank-zero lattice gives L_0≤T^ L_0 . For a sublattice M⊂L/L_0 , lift it to M as in Lemma 8 ([Orthogonal lattice quotients]). Minimality gives L_0 T^ L_0 ≤ M T^ L_0+ M = L_0\, M T^ L_0+ M , which proves the quotient bound. Under the additional hypothesis, writing k= L_0 , the two bounds on L_0 give e^ -Δ T_0^k≤T^k . Taking logarithms proves the rank bound.