CCDN Theorem 4 with the corrected degree exponent of Remark 4.3.8. In N = n + 3 variables the exponent is 18 + 3n = 3N + 9: the corrected surface bound d^18 and a cost of d^3 for each bounded good hyperplane slice (affineHypersurfaceGrowth, in CCDN.Hypersurface.AffineHypersurfaceCount).

theorem CCDN.affine_hypersurface_dimension_growth (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin (n + 3)) ℤ), HasAbsIrreducibleTopForm f → 5 ≤ f.totalDegree → ∀ (B : ℝ), 1 ≤ B → ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ C * ↑f.totalDegree ^ (18 + 3 * n) * B ^ (n + 1)

CCDN Theorem 4 for integer equations in all affine ambient dimensions at least three. The constant depends only on dimension, and the explicit degree exponent is 18 + 3n in n+3 variables.

theorem CCDN.affine_hypersurface_dimension_growth_rat (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin (n + 3)) ℚ), HasAbsIrreducibleTopFormRat f → 5 ≤ f.totalDegree → ∀ (B : ℝ), 1 ≤ B → ↑(count (zeroLocus f) B) ≤ C * ↑f.totalDegree ^ (18 + 3 * n) * B ^ (n + 1)

CCDN Theorem 4 for rational equations, with the degree exponent 18 + 3n in n+3 variables.