The odd-degree branch of CCDN Theorem 6 for the ideal-class group, via the lattice, bounded representatives, translation classes, and signed norm curves of the imported files.

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

A coefficient depending only on the field degree.

Equations

• CCDN.oddDegreeClassGroupConstant n = 12 * CCDN.affineHypersurfaceAuxiliaryConstant 0 * ↑n ^ 4 * (CCDN.numberFieldLatticeBoxConstant n (↑n ^ 3) * 2 ^ n) * (3 * 9 ^ (n - 1))

theorem CCDN.odd_degree_classGroup_two_torsion_bound (K : Type u_1) [Field K] [NumberField K] (hn : 2 ≤ Module.finrank ℚ K) (hodd : Odd (Module.finrank ℚ K)) : ↑(classGroupTwoTorsionCard K) ≤ oddDegreeClassGroupConstant (Module.finrank ℚ K) * |↑(NumberField.discr K)| ^ (1 / 2 - 1 / (2 * ↑(Module.finrank ℚ K)))

The log-free odd-degree bound.