Uniform numerical absorption for quadratic class-group descent. The prime-factor and logarithmic losses fit in the positive exponent margin between the base-field and extension-field estimates.

theorem CCDN.quadratic_class_group_numeric_descent (m : ℕ) (hm : 2 ≤ m) (C : ℝ) (hC : 0 < C) : ∃ (A : ℝ), 0 < A ∧ ∀ (D : ℕ), 1 ≤ D → ∀ (x h H : ℝ), 1 ≤ x → x ^ 2 ≤ ↑D → 0 ≤ h → h ≤ C * x ^ (1 / 2 - 1 / (2 * ↑m)) * (Real.log x + 1) → H ≤ (h * 2 ^ (2 * m * D.primeFactors.card + m)) ^ 2 → H ≤ A * ↑D ^ (1 / 2 - 1 / (2 * ↑(2 * m)))

Exact numerical quadratic descent. The constant is chosen before the discriminant, base discriminant, and class-group cardinalities. There is no logarithmic loss in the conclusion.

theorem CCDN.quadratic_class_group_base_numeric : ∃ (C : ℝ), 0 < C ∧ ∀ (D : ℕ), 1 ≤ D → 2 ^ (4 * D.primeFactors.card + 2) ≤ C * ↑D ^ (1 / 4)

The explicit quadratic-field genus bound already implies the degree-two power bound needed to start degree induction.