Section 6, Lemma 6.1: an absolutely irreducible rational equation of prescribed degree vanishes on the entire stated integer box.

theorem CCDN.exists_irreducible_zero_one_equation {K : Type u_1} {L : Type u_2} [Field K] [Field L] (φ : K →+* L) (d n : ℕ) (hd : 0 < d) (hn : 2 ≤ n) : ∃ (f : MvPolynomial (Fin n) K), f.totalDegree = d ∧ Irreducible ((MvPolynomial.map φ) f) ∧ (MvPolynomial.eval 0) f = 0 ∧ (MvPolynomial.eval fun (x : Fin n) => 1) f = 0

For d > 0 and n ≥ 2, there is a polynomial over K in n variables of total degree d that stays irreducible over L along φ : K →+* L and vanishes at both 0 and (1, …, 1).

theorem CCDN.exists_irreducible_origin_equation {K : Type u_1} {L : Type u_2} [Field K] [Field L] (φ : K →+* L) (d n : ℕ) (hd : 0 < d) (hn : 2 ≤ n) : ∃ (f : MvPolynomial (Fin n) K), f.totalDegree = d ∧ Irreducible ((MvPolynomial.map φ) f) ∧ (MvPolynomial.eval 0) f = 0

For d > 0 and n ≥ 2, there is a polynomial over K in n variables of total degree d that stays irreducible over L along φ : K →+* L and vanishes at the origin; this supplies the degree-d examples in every positive degree of CCDN Section 6.

theorem CCDN.exists_absolutely_irreducible_integer_grid (d n : ℕ) (hd : 1 ≤ d) (hn : 2 ≤ n) : ∃ (f : MvPolynomial (Fin n) ℚ), f.totalDegree = d ∧ AbsolutelyIrreducibleRat f ∧ ∀ (z : IntPoint n), (∀ (i : Fin n), |z i| ≤ ↑((d - 1) / (2 * n))) → (MvPolynomial.eval (rationalPoint z)) f = 0

CCDN Lemma 6.1. The radius is exactly floor((d−1)/(2n)).