A proper section bounds independent classes in any algebra-valued image, not only distinct point evaluations. This is the multiplicity-ready form of the Hilbert-function argument.
theorem
CCDN.section_image_rank_le
{K : Type u_1}
{B : Type u_2}
{σ : Type u_3}
{ι : Type u_4}
[Field K]
[CommRing B]
[Algebra K B]
[Finite σ]
[Fintype ι]
(p : Ideal (MvPolynomial σ K))
[p.IsPrime]
(d : ℕ)
(hdegree : HasFilteredCurveDegree p d)
(φ : MvPolynomial σ K ⧸ p →ₐ[K] B)
(h : ι → MvPolynomial σ K)
(hlin : LinearIndependent K fun (i : ι) => φ ((Ideal.Quotient.mk p) (h i)))
(l : MvPolynomial σ K)
(hl : l ∉ p)
(m : ℕ)
(hld : l.totalDegree ≤ m)
(hzero : φ ((Ideal.Quotient.mk p) l) = 0)
:
Independent polynomial images in a proper section number at most d*m. This applies to truncated local expansions as well as to point values.