Distinct-point bounds obtained from the auxiliary polynomials and Bézout. The sharp finite-field estimate remains an explicit hypothesis.

theorem CCDN.rational_map_totalDegree {σ : Type u_1} (f : MvPolynomial σ ℤ) : ((MvPolynomial.map (Int.castRingHom ℚ)) f).totalDegree = f.totalDegree

Mapping an integer polynomial to ℚ preserves its total degree.

theorem CCDN.rational_irreducible_of_charZero_map {F : Type u_1} {σ : Type u_2} [Field F] [CharZero F] (f : MvPolynomial σ ℤ) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f)) : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)

If the image of an integer polynomial in a field F of characteristic zero is irreducible, then its image over ℚ is irreducible.

theorem CCDN.plane_chart_points_card_le_auxiliary_degree {d M t : ℕ} (f g : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hg : g.IsHomogeneous M) (hprim : PrimitiveIntegerPolynomial f) (hdchart : ((affineChart 2) f).totalDegree = d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) ((affineChart 2) f))) (hnd : ¬f ∣ g) (z : Fin t → Fin 2 → ℤ) (hinj : Function.Injective z) (hzf : ∀ (i : Fin t), (MvPolynomial.eval (z i)) ((affineChart 2) f) = 0) (hzg : ∀ (i : Fin t), (MvPolynomial.eval (Fin.cons 1 (z i))) g = 0) : t ≤ d * M

The precise Bézout step for a homogeneous integer auxiliary polynomial and a primitive equation whose chart has full degree.

theorem CCDN.integer_zero_count_le_of_family_bound {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (B R : ℝ) (hbound : ∀ (t : ℕ) (z : Fin t → Fin n → ℤ), Function.Injective z → (∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) → (∀ (i : Fin t), InBox (z i) B) → ↑t ≤ R) : ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ R

Enumerating the integer zeros transfers finite-family bounds to the counting interface, including empty point sets.