The logarithmic branch of CCDN Theorem 6 for number fields with no index-two intermediate field. All ideal-class representatives, curves, lattice points and exceptional subfields are constructed and counted.

Uniform finite-radius counts for the ring of integers and its integer-translation classes. The required short basis is constructed, and every coefficient depends only on the degree.

theorem CCDN.boundedSquareNormTranslationClasses_uniform_count (K : Type u_1) [Field K] [NumberField K] (hn : 2 ≤ Module.finrank ℚ K) {B : ℝ} (hB1 : 1 ≤ B) (hB : |↑(NumberField.discr K)| ^ (1 / ↑(Module.finrank ℚ K)) ≤ B) : ↑(boundedSquareNormTranslationClasses K B).card * √|↑(NumberField.discr K)| ≤ numberFieldLatticeBoxConstant (Module.finrank ℚ K) (↑(Module.finrank ℚ K) ^ 3) * 2 ^ Module.finrank ℚ K * B ^ (Module.finrank ℚ K - 1)

For a number field K of degree n ≥ 2 and a radius B ≥ max 1 (|discr K| ^ (1 / n)), the number of bounded square-norm translation classes times √|discr K| is at most a constant depending only on n times B ^ (n - 1).

noncomputable def CCDN.noIndexTwoClassGroupConstant (n : ℕ) : ℝ

The degree-dependent constant in the two-torsion class-group bound for number fields of degree n without an intermediate field of index two.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.noIndexTwoClassGroupConstant_pos (n : ℕ) : 0 < noIndexTwoClassGroupConstant n

The constant noIndexTwoClassGroupConstant n is positive.

theorem CCDN.no_index_two_classGroup_two_torsion_bound (K : Type u_1) [Field K] [NumberField K] (hn : 2 ≤ Module.finrank ℚ K) (hnoTwo : ∀ (L : IntermediateField ℚ K), Module.finrank (↥L) K ≠ 2) : ↑(classGroupTwoTorsionCard K) ≤ noIndexTwoClassGroupConstant (Module.finrank ℚ K) * |↑(NumberField.discr K)| ^ (1 / 2 - 1 / (2 * ↑(Module.finrank ℚ K))) * Real.log |↑(NumberField.discr K)|

For a number field K of degree n ≥ 2 with no intermediate field L of index [K : L] = 2, the two-torsion subgroup of the class group has order at most C(n) * |discr K| ^ (1 / 2 - 1 / (2 * n)) * log |discr K|.