The odd-degree class-group counting step uses the finite translation classes and their two signed norm curves. The curve equation retains its full odd degree, including when the translating generator belongs to a proper subfield.

theorem CCDN.normCurveBoxHeight_root_le {n : ℕ} (hn : 2 ≤ n) {B : ℝ} (hB : 1 ≤ B) : max (2 * B) √(B ^ n) ^ (1 / ↑n) ≤ 2 * √B

For n ≥ 2 and B ≥ 1, the norm-curve box height H = max (2 * B) (√(B ^ n)) satisfies H ^ (1 / n) ≤ 2 * √B.

theorem CCDN.boundedSquareNormIntegers_odd_count_of_relative_short_basis (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℝ (NumberField.mixedEmbedding.euclidean.mixedSpace K)) (hb : ∀ (i : ι), b i ∈ NumberField.mixedEmbedding.euclidean.integerLattice K) (hn : 2 ≤ Module.finrank ℚ K) (hodd : Odd (Module.finrank ℚ K)) {B C : ℝ} (hB : 1 ≤ B) (hC : 0 ≤ C) (hnorm : ∀ (i : ι), ‖b i‖ ≤ C * B) : ↑(boundedSquareNormIntegers K B).ncard * √|↑(NumberField.discr K)| ≤ 12 * affineHypersurfaceAuxiliaryConstant 0 * ↑(Module.finrank ℚ K) ^ 4 * (numberFieldLatticeBoxConstant (Module.finrank ℚ K) C * 2 ^ Module.finrank ℚ K) * (B ^ (Module.finrank ℚ K - 1) * √B)

The algebraic and curve-counting reduction combined with the finite lattice packing, given a short integral basis b.