Nonsingular integer points have many smooth reduction primes in one common finite window. The excluded primes divide one nonzero partial derivative value, whose height is bounded directly from the equation.

theorem CCDN.exists_smooth_prime_window_subset {n : ℕ} (f : MvPolynomial (Fin n) ℤ) {H B L : ℝ} (hH : 1 ≤ H) (hB : 1 ≤ B) (hL : 1 ≤ L) (hcoeff : CoefficientHeightLE f H) (hheight : (↑n + 1) * Real.log (↑f.totalDegree + 1) + Real.log H + ↑f.totalDegree * Real.log B ≤ L) (x : IntPoint n) (hx : InBox x B) (hsmooth : ∃ (j : Fin n), (MvPolynomial.eval x) ((MvPolynomial.pderiv j) f) ≠ 0) : ∃ P ⊆ congruencePrimeWindow L, Real.exp L ≤ ∏ p ∈ P, ↑p ∧ ∀ p ∈ P, ∃ (j : Fin n), (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0

If x is an integer point of the box at which some partial derivative of f is nonzero, and L dominates the logarithmic size of such a derivative, then the prime window of logarithmic size L contains a set of primes with product at least exp L modulo each of which x is a smooth point of f.