A good integer hyperplane normal of height at most d³, obtained from the universal Noether detector and integer-grid avoidance.

theorem CCDN.exists_geometrically_good_hyperplane {n : ℕ} (f : MvPolynomial (Option (Fin (3 + n))) ℤ) (d : ℕ) (hd : 2 ≤ d) (hf : f.IsHomogeneous d) (hir : AbsolutelyIrreducible f) : ∃ (D : ℤ) (a : Fin (3 + n) → ℤ), D ≠ 0 ∧ |D| ≤ ↑(d ^ 3) ∧ (∀ (i : Fin (3 + n)), |a i| ≤ ↑(d ^ 3)) ∧ ((graphHyperplaneRestriction fun (i : Fin (3 + n)) => ↑(a i) / ↑D) ((MvPolynomial.map (Int.castRingHom ℚ)) f)).totalDegree = d ∧ AbsolutelyIrreducibleRat ((graphHyperplaneRestriction fun (i : Fin (3 + n)) => ↑(a i) / ↑D) ((MvPolynomial.map (Int.castRingHom ℚ)) f))

Full-degree geometrically integral hyperplane restriction, with a cubic integer normal bound independent of the coefficients and ambient dimension.