A logarithm-free plane-curve estimate in terms of the geometric bad-prime factor. Uniformly bounded bad-prime factors therefore give a coefficient-independent logarithm-free counting theorem.

theorem CCDN.affine_plane_count_bad_prime (f : MvPolynomial (Fin 2) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) (hd : 0 < f.totalDegree) {B : ℝ} (hB : 1 ≤ B) : ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ affineHypersurfaceAuxiliaryConstant 0 * ↑f.totalDegree ^ 4 * (hypersurfaceBadPrimeFactor f + 2) * B ^ (1 / ↑f.totalDegree)

The plane auxiliary and Bezout prove the bad-prime bound for integer zeros.