Polynomial parameters of degree at most q have function-field degree at most the Hilbert multiplicity times q to the dimension.
theorem
CCDN.hilbert_scaled_block_count_le_multiplicity
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
(hI : I ≠ ⊤)
(m d r D q : ℕ)
(hq : 0 < q)
(hdimdeg : HasAffineDimensionDegree I m d)
(hlow : ∀ (N : ℕ), r * (m + N).choose m ≤ Module.finrank K ↥(filteredCoordinateSpace I (D + q * N)))
:
If I has affine dimension m and degree d, and r · (m + N).choose m is at most the affine
Hilbert function of I at D + q N for all N, then r ≤ d · q ^ m.