Hilbert inequalities for a proper polynomial section of a prime affine variety. Multiplication by the section is injective in the original coordinate domain and is killed in the section quotient.

theorem CCDN.proper_section_hilbert_polynomial_difference {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) [I.IsPrime] (f : MvPolynomial σ K) (hf : f ∉ I) : ∃ (M : ℕ), ∀ N ≥ M, Polynomial.eval (↑N) ((filteredHilbertPolynomial (I ⊔ Ideal.span {f})).comp (Polynomial.X + Polynomial.C ↑f.totalDegree)) ≤ Polynomial.eval (↑N) ((filteredHilbertPolynomial I).comp (Polynomial.X + Polynomial.C ↑f.totalDegree) - filteredHilbertPolynomial I)

The Hilbert polynomial of the section is bounded by the finite difference of the original Hilbert polynomial, with the necessary shift.

theorem CCDN.proper_section_hilbert_dimension_leadingCoeff {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) [I.IsPrime] (m : ℕ) (hdim : (filteredHilbertPolynomial I).natDegree = m + 1) (f : MvPolynomial σ K) (hf : f ∉ I) (hfdeg : 0 < f.totalDegree) (hsection : I ⊔ Ideal.span {f} ≠ ⊤) : (filteredHilbertPolynomial (I ⊔ Ideal.span {f})).natDegree ≤ m ∧ ((filteredHilbertPolynomial (I ⊔ Ideal.span {f})).natDegree = m → (filteredHilbertPolynomial (I ⊔ Ideal.span {f})).leadingCoeff ≤ (filteredHilbertPolynomial I).leadingCoeff * (↑m + 1) * ↑f.totalDegree)

Every proper polynomial section lowers the affine Hilbert dimension by at least one. In the maximal remaining dimension its leading coefficient is at most the expected intersection degree.