The affine auxiliary polynomial obtained from a prime-scaled homogeneous model. All point and nondivisibility transports are proved.

theorem CCDN.scaled_auxiliary_vanishes {n M : ℕ} (f : MvPolynomial (Fin n) ℤ) (G : MvPolynomial (Fin (n + 1)) ℤ) (hGhom : G.IsHomogeneous M) (h : ℤ) (hh : h ≠ 0) {B : ℝ} (hscale : |↑h| ≤ B) (hGzero : ∀ (P : ProjectivePoint n), Projectivization.mulHeight P ≤ B → P ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) (scaledHomogenize f.totalDegree h f)) → P ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) G)) (x : IntPoint n) : InBox x B → (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval x) ((homogeneousSlice n h) G) = 0

A nonzero bounded scaling coordinate transfers projective vanishing to the affine box.

theorem CCDN.prime_scaled_affine_auxiliary {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible f) (hd : 0 < f.totalDegree) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) {B : ℝ} (hB : 1 ≤ B) (hpB : ↑p ≤ B) : ∃ (g : MvPolynomial (Fin (n + 2)) ℤ), IsBoxAuxiliary f g B ∧ ↑g.totalDegree ≤ hypersurfaceAuxiliaryDegreeBound n f.totalDegree B (hypersurfaceBadPrimeFactor (scaledHomogenize f.totalDegree (↑p) f)) ↑(integerCoefficientHeight (scaledHomogenize f.totalDegree (↑p) f))

For any prime p<=B avoiding the constant coefficient, construct an affine auxiliary nonmultiple. The degree retains the exact height and bad-prime factor of the scaled model, ready for their quantitative estimates.