Absolutely irreducible plane equations through arbitrary finite square Cartesian grids. Translation moves the Eisenstein place away from the grid.

theorem CCDN.exists_absolutely_irreducible_plane_grid {K : Type u_1} {L : Type u_2} [Field K] [Infinite K] [Field L] (φ : K →+* L) (s : Finset K) (hs : 0 < s.card) (d : ℕ) (hd : s.card + 2 ≤ d) (hsize : 2 * s.card ≤ d + 1) : ∃ (f : MvPolynomial (Fin 2) K), f.totalDegree = d ∧ Irreducible ((MvPolynomial.map φ) f) ∧ ∀ (z : Fin 2 → K), (∀ (i : Fin 2), z i ∈ s) → (MvPolynomial.eval z) f = 0

An arbitrary finite square grid of side s lies on an absolutely irreducible curve of every degree d≥s+2 satisfying 2s≤d+1, given by an explicit equation.