Uniform class-group bounds by strong induction on the field degree. A quadratic subfield has smaller degree, and discriminant descent leaves enough exponent saving to absorb the proved ramification factor. The coefficient is chosen before the field.

Degree and discriminant facts used to assemble the class-group bound by strong induction on the number-field degree.

def CCDN.ClassGroupLogarithmicBound (n : ℕ) (C : ℝ) : Prop

The statement that every number field K of degree n satisfies h₂(K) ≤ C * |discr K| ^ (1 / 2 - 1 / (2 * n)) * (log |discr K| + 1).

Equations

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

theorem CCDN.classGroup_uniform_logarithmic_bound (n : ℕ) (hn : 2 ≤ n) : ∃ (C : ℝ), 0 < C ∧ ClassGroupLogarithmicBound n C

For every n ≥ 2 there is a constant C > 0 such that every number field K of degree n satisfies h₂(K) ≤ C * |discr K| ^ (1 / 2 - 1 / (2 * n)) * (log |discr K| + 1).