The certified affine Hilbert degree bounds the number of geometric infinity points in each normalized projective chart.

Homogeneous polynomials with extension-field coefficients contribute no new directions beyond the extension-field span of ground-field monomials.

Finite interpolation in a projective affine chart can be performed by homogeneous polynomials of any sufficiently large common degree.

Evaluating homogeneous polynomials at geometric infinity points has L-linear rank at most the corresponding infinity Hilbert piece. The source curve and its Hilbert function are defined over the original field K.

theorem CCDN.exists_finite_infinity_chart {K : Type u_1} {L : Type u_2} {σ : Type u_3} [Field K] [Field L] [Algebra K L] [Finite σ] (I : Ideal (MvPolynomial σ K)) (d : ℕ) (hdegree : HasFilteredCurveDegree I d) (j : σ) : ∃ (S : Finset (σ → L)), S.card ≤ d ∧ ∀ (z : σ → L), z ∈ S ↔ z ∈ MvPolynomial.zeroLocus L (leadingInfinityIdeal I) ∧ z j = 1

Each normalized infinity chart is a finite set with at most d points, not merely a bound for already finite subsets.