Identically zero sections are bounded separately using their three defining points. This gives three powers of the field size in the denominator, even with degenerate parameterizations included.

theorem CCDN.finite_field_polynomial_zeros_card {K : Type u_1} {τ : Type u_2} [Field K] [Fintype K] [Fintype τ] [Nonempty τ] (f : MvPolynomial τ K) (hf : f ≠ 0) : Nat.card { x : τ → K // (MvPolynomial.eval x) f = 0 } ≤ f.totalDegree * Fintype.card K ^ (Fintype.card τ - 1)

The usual degree-times-q^(m-1) bound, for arbitrary nonempty finite coordinate types and affine zeros.

def CCDN.ZeroPlaneParameters {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) : Type (max 0 u_1 u_2)

All parameter triples whose restricted polynomial is identically zero.

Equations

• CCDN.ZeroPlaneParameters f = { v : CCDN.PlaneParameters σ → K // CCDN.universalPlaneSection f v = 0 }

theorem CCDN.finite_field_zero_plane_parameters_card {K : Type u_1} {σ : Type u_2} [Field K] [Fintype K] [Fintype σ] (f : MvPolynomial (Option σ) K) (hf : f ≠ 0) : Nat.card (ZeroPlaneParameters f) ≤ f.totalDegree ^ 3 * Fintype.card K ^ (3 * Fintype.card σ)

In m ambient coordinates, zero restrictions have at most d^3q^(3m-3) parameter triples. This is substantially smaller than the general bad-plane bound and controls their q^2-point contribution to incidence averaging.