CCDN Theorem 6 for the two-torsion subgroup of the ideal class group. Constants are uniform over all number fields of the given degree. Odd degrees have no logarithm; even degrees have exactly one logarithm. The quadratic descent, exceptional subfields, lattice and curve counts used by the proof are all proved in the imported modules.

theorem CCDN.classGroup_two_torsion_bound (n : ℕ) (hn : 3 ≤ n) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : Type u) [inst : Field K] [inst_1 : NumberField K], Module.finrank ℚ K = n → ↑(classGroupTwoTorsionCard K) ≤ C * |↑(NumberField.discr K)| ^ (1 / 2 - 1 / (2 * ↑n)) * Real.log |↑(NumberField.discr K)| ^ (1 - n % 2)

The full class-group application, including the logarithmic exponent specified by the parity of the field degree.