The scaling-prime interval yields the affine box exponent 1/d. These numerical bounds are independent of the coefficient height.

theorem CCDN.scaled_plane_finite_count_one_over_degree {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {t : ℕ} (f : MvPolynomial (Fin 2) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f)) (hd : 0 < f.totalDegree) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) (z : Fin t → Fin 2 → ℤ) (hinj : Function.Injective z) {A B C : ℝ} (hzB : IsBoxZeroFamily f B z) (hA : 1 ≤ A) (hpB : ↑p ≤ B) (hBp : B ≤ A * ↑p) (hC : 0 ≤ C) (hcount : PlaneResidueCountBound C f.totalDegree f) : ↑t ≤ (38 + 8 * Real.exp (heightDeterminantError C + 20) + 2 * Real.exp (heightDeterminantError C + 23) * Real.exp 14 * Real.exp 2 * A) * ↑f.totalDegree ^ 3 * B ^ (1 / ↑f.totalDegree) * (Real.log B + ↑f.totalDegree)

A coefficient-uniform affine count with exponent 1/d, conditional on the sharp finite-field estimate and a prime p in [B/A,B] not dividing f(0).