The bounded square-norm set is partitioned by integer translations. This constructs a finite norm-curve family. The uniform estimate for the number of translation classes is a separate lattice theorem.

@[reducible, inline]

abbrev CCDN.IntegerTranslationQuotient (K : Type u_1) [Field K] : Type u_1

The quotient of 𝓞 K by the additive subgroup of rational integers, whose classes are the orbits under integer translation.

Equations

• CCDN.IntegerTranslationQuotient K = (NumberField.RingOfIntegers K ⧸ AddSubgroup.zmultiples 1)

noncomputable def CCDN.boundedSquareNormTranslationClasses (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Finset (IntegerTranslationQuotient K)

The finite set of integer-translation classes of the bounded square-norm integers boundedSquareNormIntegers K B.

Equations

• CCDN.boundedSquareNormTranslationClasses K B = Finset.image (fun (α : NumberField.RingOfIntegers K) => ↑α) ⋯.toFinset

theorem CCDN.exists_norm_translate_cover (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : ∃ (β : ↥(boundedSquareNormTranslationClasses K B) → NumberField.RingOfIntegers K), Function.Injective β ∧ (∀ (q : ↥(boundedSquareNormTranslationClasses K B)) (w : NumberField.InfinitePlace K), w ↑(β q) ≤ B) ∧ ∀ α ∈ boundedSquareNormIntegers K B, ∃ (q : ↥(boundedSquareNormTranslationClasses K B)), α ∈ squareNormTranslateFiber K (β q) B

Bounded square-norm integers admit injective bounded representatives whose integer translation fibres cover the original set.

theorem CCDN.exists_norm_curve_family (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : ∃ (β : ↥(boundedSquareNormTranslationClasses K B) → NumberField.RingOfIntegers K), Function.Injective β ∧ (∀ (q : ↥(boundedSquareNormTranslationClasses K B)) (w : NumberField.InfinitePlace K), w ↑(β q) ≤ B) ∧ (boundedSquareNormIntegers K B).ncard ≤ ∑ q : ↥(boundedSquareNormTranslationClasses K B), (count (signedNormCurveLocus K (β q) 1) (max (2 * B) √(B ^ Module.finrank ℚ K)) + count (signedNormCurveLocus K (β q) (-1)) (max (2 * B) √(B ^ Module.finrank ℚ K)))

There is an injective family of algebraic integers β q bounded by B at every infinite place, indexed by the bounded square-norm translation classes, such that the number of bounded square-norm integers is at most the total number of points of height at most max (2 * B) (√(B ^ n)) on the signed norm curves for β q with signs ±1.