Additivity of the leading filtered dimension bounds the total degree of the minimal-prime components of a two-equation section.

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

The additive degree inequality in the rational curve-degree interface.