Proper affine sections and Bézout counts from prime-scaled homogeneous models. The coordinate slice is x₀=p, and the original points stay integral.

theorem CCDN.scaled_auxiliary_rational_not_dvd {n M : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf0 : f ≠ 0) (hprim : PrimitiveIntegerPolynomial f) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) (g : MvPolynomial (Fin (n + 1)) ℤ) (hg : g.IsHomogeneous M) (hnd : ¬scaledHomogenize f.totalDegree (↑p) f ∣ g) : ¬(MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) ((homogeneousSlice n ↑p) g)

Let p be a prime not dividing the constant coefficient of the primitive integer polynomial f. If a form g is not divisible by the p-scaled homogenization of f, then over ℚ its slice at x₀ = p is not divisible by f.

theorem CCDN.scaled_plane_points_card_le_auxiliary_degree {M t : ℕ} (f : MvPolynomial (Fin 2) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) (g : MvPolynomial (Fin 3) ℤ) (hg : g.IsHomogeneous M) (hnd : ¬scaledHomogenize f.totalDegree (↑p) f ∣ g) (z : Fin t → Fin 2 → ℤ) (hinj : Function.Injective z) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) (hzg : ∀ (i : Fin t), (MvPolynomial.eval (Fin.cons (↑p) (z i))) g = 0) : t ≤ f.totalDegree * M

Once a homogeneous auxiliary nonmultiple has been constructed on the prime-scaled model, its degree gives the original-plane point bound.