Integer equations for every parallel level of a constructed good hyperplane. Degrees and geometric irreducibility of the leading forms are preserved, and deleting the solved coordinate does not enlarge the box.

theorem CCDN.exists_integer_model_absolute_top {n : ℕ} (f : MvPolynomial (Fin n) ℚ) (hir : Irreducible ((MvPolynomial.map (algebraMap ℚ (AlgebraicClosure ℚ))) ((MvPolynomial.homogeneousComponent f.totalDegree) f))) : ∃ (g : MvPolynomial (Fin n) ℤ), g.totalDegree = f.totalDegree ∧ Irreducible ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure ℚ))) ((MvPolynomial.homogeneousComponent g.totalDegree) g)) ∧ ∀ (x : Fin n → ℤ), (MvPolynomial.eval x) g = 0 ↔ (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) f = 0

A rational polynomial whose top-degree form is absolutely irreducible has an integer model of the same total degree, also with absolutely irreducible top-degree form, that has the same integer zeros.

theorem CCDN.exists_integer_hyperplane_slice_models {n : ℕ} (f : MvPolynomial (Option (Fin n)) ℤ) (D : ℤ) (a : Fin n → ℤ) (hD : D ≠ 0) (hgood : Irreducible ((MvPolynomial.map (algebraMap ℚ (AlgebraicClosure ℚ))) ((graphHyperplaneRestriction fun (i : Fin n) => ↑(a i) / ↑D) ((MvPolynomial.map (Int.castRingHom ℚ)) ((MvPolynomial.homogeneousComponent f.totalDegree) f))))) : ∃ (g : ℤ → MvPolynomial (Fin n) ℤ), ∀ (k : ℤ), (g k).totalDegree = f.totalDegree ∧ Irreducible ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure ℚ))) ((MvPolynomial.homogeneousComponent (g k).totalDegree) (g k))) ∧ ∀ (x : Option (Fin n) → ℤ), D * x none - ∑ i : Fin n, a i * x (some i) = k → (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval fun (i : Fin n) => x (some i)) (g k) = 0

Integer models for all parallel slices of any chosen good rational hyperplane; the normal may come from any quantitative construction.