Degree and proper-section budgets for any finite family of distinct prime curves on a surface section. A curve constructed by another auxiliary is counted as a component of the section whenever its ideal contains the section's equation.

theorem CCDN.surface_prime_curve_degree_sum_le (f g : CoordinatePolynomial 3) (hf : Irreducible f) (hfg : ¬f ∣ g) (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ) (hS : ∀ P ∈ S, IsSurfaceCurve f P (δ P) ∧ g ∈ P) : ∑ P ∈ S, δ P ≤ MvPolynomial.totalDegree f * MvPolynomial.totalDegree g

Distinct prime curves of height two contained in a proper surface section have total degree at most the product of the equation degrees.

theorem CCDN.surface_curve_crossing_count_le (f g h : CoordinatePolynomial 3) (hf : Irreducible f) (hfg : ¬f ∣ g) (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ) (hS : ∀ P ∈ S, IsSurfaceCurve f P (δ P) ∧ g ∈ P) (B : ℝ) : count (⋃ P ∈ {P ∈ S | h ∉ P}, idealZeroLocus P ∩ zeroLocus h) B ≤ MvPolynomial.totalDegree f * MvPolynomial.totalDegree g * MvPolynomial.totalDegree h

For curves P ∈ S on the irreducible surface f = 0 whose ideals contain g (with f not dividing g), the integral points of height at most B on h = 0 lying on those curves whose ideals do not contain h number at most deg f * deg g * deg h.