A finite decomposition of a proper affine surface section into rational prime curves, with a proved additive degree budget. Components with no rational points are discarded before requiring positive curve degrees.

An eventual linear upper bound gives an eventual linear Hilbert formula, with its slope bounded by the original coefficient.

theorem CCDN.polynomialSection_minimalPrime_degrees_exist (f g : CoordinatePolynomial 3) (hf : Irreducible f) (hfg : ¬f ∣ g) : ∃ (d : ↥(minimalPrimeComponents (polynomialSectionIdeal f g)) → ℕ), (∀ (P : ↥(minimalPrimeComponents (polynomialSectionIdeal f g))), HasAffineCurveDegree (↑P) (d P)) ∧ ∑ P : ↥(minimalPrimeComponents (polynomialSectionIdeal f g)), d P ≤ MvPolynomial.totalDegree f * MvPolynomial.totalDegree g

Every minimal-prime component has an eventual affine Hilbert degree. The slope is allowed to be zero until a rational point is exhibited.

theorem CCDN.exists_completeIntersection_curve_components (f g : CoordinatePolynomial 3) (hf : Irreducible f) (hfg : ¬f ∣ g) : ∃ (S : Finset (Ideal (CoordinatePolynomial 3))) (d : Ideal (CoordinatePolynomial 3) → ℕ), (∀ P ∈ S, IsSectionCurve f g P (d P)) ∧ zeroLocus f ∩ zeroLocus g = ⋃ P ∈ S, idealZeroLocus P ∧ ∑ P ∈ S, d P ≤ MvPolynomial.totalDegree f * MvPolynomial.totalDegree g ∧ ∀ P ∈ S, (polynomialSectionIdeal f g).IsMinimalPrime P

A proper section in affine three-space is covered exactly by a finite set of rational prime curves. Their positive Hilbert degrees sum to at most the product of the two equation degrees. All components and degrees are constructed, including the case of an empty common zero set.