A coordinate-grid bound for a proper complete intersection. The constant depends only on the ambient dimension; the degree dependence is quadratic.

theorem CCDN.proper_intersection_grid_card_le {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] {n d : ℕ} (f g : MvPolynomial (Fin (n + 2)) K) (hf : Prime f) (hfg : ¬f ∣ g) (hfd : f.totalDegree ≤ d) (hgd : g.totalDegree ≤ d) (S : Finset K) (z : ι → Fin (n + 2) → K) (hz : Function.Injective z) (hzS : ∀ (i : ι) (j : Fin (n + 2)), z i j ∈ S) (hzf : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0) (hzg : ∀ (i : ι), (MvPolynomial.eval (z i)) g = 0) : Fintype.card ι ≤ (n + 2) ^ n * d ^ 2 * S.card ^ n

If f is prime, g is not divisible by f, and both have total degree at most d, then the number of distinct common zeros of f and g in the grid Sⁿ⁺² is at most (n + 2) ^ n · d² · |S| ^ n.