Finite-field point bounds for a proper section of an irreducible hypersurface. The proof uses polynomial interpolation and the filtered Koszul rank estimate.

theorem CCDN.finite_field_common_zeros_card_le {K : Type u_1} {ι : Type u_2} [Field K] [Fintype K] [Fintype ι] {n : ℕ} (f g : MvPolynomial (Fin (n + 2)) K) (hf : Prime f) (hfg : ¬f ∣ g) (hdegrees : f.totalDegree + g.totalDegree ≤ 2 * (Fintype.card K - 1)) (z : ι → Fin (n + 2) → K) (hz : Function.Injective z) (hzf : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0) (hzg : ∀ (i : ι), (MvPolynomial.eval (z i)) g = 0) : Fintype.card ι ≤ (n + 4) ^ n * f.totalDegree * g.totalDegree * Fintype.card K ^ n

Below the field-size degree threshold, a dimension-only constant times (degree f)(degree g) q^(ambient dimension-2) bounds the common zeros.