The exact affine Hilbert function of a principal plane equation. This identifies polynomial total degree with the degree in the curve-counting target.

theorem CCDN.principal_filtered_finrank {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (f : MvPolynomial σ K) (hf : f ≠ 0) {N : ℕ} (hN : f.totalDegree ≤ N) : Module.finrank K ↥(filteredCoordinateSpace (Ideal.span {f}) N) + Module.finrank K ↥(MvPolynomial.restrictTotalDegree σ K (N - f.totalDegree)) = Module.finrank K ↥(MvPolynomial.restrictTotalDegree σ K N)

For f ≠ 0 and deg f ≤ N, the affine Hilbert function of (f) at N plus the dimension of the polynomials of degree at most N - deg f equals the dimension of the polynomials of degree at most N.

theorem CCDN.finrank_restrictTotalDegree_two {K : Type u_1} [Field K] (N : ℕ) : Module.finrank K ↥(MvPolynomial.restrictTotalDegree (Fin 2) K N) = (N + 2).choose 2

The polynomials in two variables of total degree at most N form a space of dimension (N + 2).choose 2.

theorem CCDN.two_mul_choose_add_two (n : ℕ) : 2 * (n + 2).choose 2 = (n + 2) * (n + 1)

2 · (n + 2).choose 2 = (n + 2)(n + 1).

theorem CCDN.choose_two_difference_eq_linear {k d N : ℕ} (hN : d ≤ N) (h : k + (N - d + 2).choose 2 = (N + 2).choose 2) : ↑k = ↑d * ↑N + (↑d - ↑(d.choose 2))

Subtracting the two plane monomial counts gives the linear degree formula.

theorem CCDN.principal_plane_hilbert_function {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (hf : f ≠ 0) {N : ℕ} (hN : f.totalDegree ≤ N) : ↑(Module.finrank K ↥(filteredCoordinateSpace (Ideal.span {f}) N)) = ↑f.totalDegree * ↑N + (↑f.totalDegree - ↑(f.totalDegree.choose 2))

The affine Hilbert function of a nonzero plane equation f of degree d is d N + d - d(d-1)/2 for every N ≥ d.