Two finite differences of a binomial Hilbert function. This gives a coefficient-uniform codimension-two bound for filtered coordinate spaces.

theorem CCDN.filteredCoordinateSpace_codim_two_bound {K : Type u_1} [Field K] {n N : ℕ} {f g : MvPolynomial (Fin (n + 2)) K} (hf : Prime f) (hfg : ¬f ∣ g) (I : Ideal (MvPolynomial (Fin (n + 2)) K)) (hIf : f ∈ I) (hIg : g ∈ I) (hN : f.totalDegree + g.totalDegree ≤ N) : Module.finrank K ↥(filteredCoordinateSpace I N) ≤ f.totalDegree * g.totalDegree * (n + N).choose n

The filtered Koszul bound reduces to a codimension-two binomial count.