The filtered Hilbert polynomial of a principal hypersurface. Its dimension and multiplicity follow from the exact finite-dimensional principal-ideal rank identity, without geometric hypotheses.

theorem CCDN.principal_filteredHilbertPolynomial_degree_leadingCoeff {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f ≠ 0) (hd : 0 < f.totalDegree) : HasAffineDimensionDegree (Ideal.span {f}) n f.totalDegree

A nonconstant principal equation in n+1 variables has filtered Hilbert dimension n and multiplicity equal to its total degree.

theorem CCDN.principal_filteredHilbertPolynomial_natDegree {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f ≠ 0) (hd : 0 < f.totalDegree) : (filteredHilbertPolynomial (Ideal.span {f})).natDegree = n

The filtered Hilbert polynomial of a nonconstant principal ideal (f) in n + 1 variables has degree n.

theorem CCDN.principal_filteredHilbertPolynomial_leadingCoeff {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f ≠ 0) (hd : 0 < f.totalDegree) : (filteredHilbertPolynomial (Ideal.span {f})).leadingCoeff = ↑f.totalDegree / ↑n.factorial

The filtered Hilbert polynomial of a nonconstant principal ideal (f) in n + 1 variables has leading coefficient deg f / n!, so the hypersurface has degree deg f.