Integer translates pack each bounded square-norm translation class into the full archimedean lattice box. This isolates the remaining geometric lattice-point estimate from the already constructed norm-curve family.

def CCDN.boundedArchimedeanIntegers (K : Type u_1) [Field K] (B : ℝ) : Set (NumberField.RingOfIntegers K)

The set of algebraic integers α ∈ 𝓞 K with w α ≤ B at every infinite place w.

Equations

• CCDN.boundedArchimedeanIntegers K B = {α : NumberField.RingOfIntegers K | ∀ (w : NumberField.InfinitePlace K), w ↑α ≤ B}

theorem CCDN.boundedArchimedeanIntegers_finite (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : (boundedArchimedeanIntegers K B).Finite

There are finitely many algebraic integers of K bounded by B at every infinite place.

theorem CCDN.boundedSquareNormTranslationClasses_packing (K : Type u_1) [Field K] [NumberField K] (B R : ℝ) : (boundedSquareNormTranslationClasses K B).card * (2 * ⌊R⌋ + 1).toNat ≤ (boundedArchimedeanIntegers K (B + R)).ncard

Translating representatives of the bounded square-norm translation classes by the integers in [-⌊R⌋, ⌊R⌋] gives distinct algebraic integers bounded by B + R at every infinite place, so the number of classes times 2 * ⌊R⌋ + 1 is at most the number of such integers.