The Stepanov point bound with an explicit finite-dimensional inequality. The polynomial bases, auxiliary coefficients, formal branches and multiplicity argument are explicit, given a numerical choice of degrees.

theorem CCDN.plane_stepanov_bound {ι : Type u_1} [Fintype ι] (p : ℕ) [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 2) (ZMod p)) (hf : Irreducible f) (hpos : 0 < f.totalDegree) (hchar : f.totalDegree < p) (z : ι → Fin 2 → ZMod p) (hz : Function.Injective z) (hzero : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0) {D A N : ℕ} (hD : f.totalDegree * D < p) (hN : N ≤ p) (hdim : ∑ r : Fin N, Module.finrank (ZMod p) ↥(filteredCoordinateSpace (Ideal.span {f}) (D + A + ↑r * f.totalDegree)) < Module.finrank (ZMod p) ↥(filteredCoordinateSpace (Ideal.span {f}) D) * Module.finrank (ZMod p) ↥(filteredCoordinateSpace (Ideal.span {f}) A)) : Fintype.card ι * N ≤ f.totalDegree * (D + p * A) + f.totalDegree * (f.totalDegree - 1) * N

Include the points where the selected partial derivative vanishes. Their number is bounded by d(d-1) using the proper derivative section.