The exact plane Hilbert function verifies the Stepanov dimension inequality for the constructed integer parameters.

theorem CCDN.stepanov_hilbert_dimension_inequality {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (hf : f ≠ 0) (p A D N : ℕ) (hd : 0 < f.totalDegree) (hp : stepanovThreshold f.totalDegree < p) (hA : f.totalDegree ≤ A) (hD : f.totalDegree ≤ D) (hx : (f.totalDegree * A) ^ 2 ≤ p) (hy : p ≤ f.totalDegree * D + f.totalDegree) (hN : N + 4 * f.totalDegree ^ 2 = f.totalDegree * A) (hNpos : 0 < N) : ∑ r : Fin N, Module.finrank K ↥(filteredCoordinateSpace (Ideal.span {f}) (D + A + ↑r * f.totalDegree)) < Module.finrank K ↥(filteredCoordinateSpace (Ideal.span {f}) D) * Module.finrank K ↥(filteredCoordinateSpace (Ideal.span {f}) A)

The numerical inequality suffices for the exact filtered dimensions.