All affine scaling, coefficient-height and zero-constant-term reductions for primitive absolutely irreducible plane equations. The resulting bound assumes the sharp finite-field estimate.

theorem CCDN.count_plane_of_residue_bound {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (f : MvPolynomial (Fin 2) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f)) (hd : 0 < f.totalDegree) {B C : ℝ} (hB : 1 ≤ B) (hC : 0 ≤ C) (hcount : PlaneResidueCountBound C f.totalDegree f) : ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ 2 * Real.exp 1 * affineNonzeroConstantBound C * curveBound f.totalDegree B

For a primitive absolutely irreducible integer plane equation, the number of integer zeros of height at most a real B ≥ 1 is bounded by a constant multiple of curveBound, assuming the finite-field point estimate p + C d² √p at primes above 27 d⁴.