The proved line contribution applies to degree-one prime components, with the original number of components as the additive cost.

A finite family of degree-one prime components gives a finite set of rational affine lines with the same rational zero-set union. Empty rational loci are discarded, and repeated line sets are counted only once.

theorem CCDN.degree_one_components_line_cover (S : Finset (Ideal (CoordinatePolynomial 3))) (hcurve : ∀ P ∈ S, P.IsPrime ∧ P.height = 2 ∧ HasAffineCurveDegree P 1) : ∃ (lines : Finset (Set (RatPoint 3))), ⋃ P ∈ S, idealZeroLocus P = ⋃ L ∈ lines, L ∧ lines.card ≤ S.card ∧ ∀ L ∈ lines, (∃ P ∈ S, L = idealZeroLocus P) ∧ ∃ (a : RatPoint 3) (v : RatPoint 3), v ≠ 0 ∧ L = rationalAffineLine a v

The union of the rational zero sets of finitely many degree-one affine curves in three-space is a union of at most as many rational affine lines, each of which is the zero set of one of the curves.

theorem CCDN.surface_degree_one_component_contribution : ∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin 3) ℤ), HasAbsIrreducibleTopForm f → 3 ≤ f.totalDegree → ∀ (B : ℝ), 0 ≤ B → ∀ (S : Finset (Ideal (CoordinatePolynomial 3))), (∀ P ∈ S, P.IsPrime ∧ P.height = 2 ∧ HasAffineCurveDegree P 1) → (∀ P ∈ S, (MvPolynomial.map (Int.castRingHom ℚ)) f ∈ P) → ↑(count (⋃ P ∈ S, idealZeroLocus P) B) ≤ C * ↑f.totalDegree ^ 6 * B + ↑S.card

There is an absolute constant C such that, for an integer surface equation f of degree d ≥ 3 with absolutely irreducible top-degree form, the integral points of height at most B on a finite family S of degree-one curves on the surface number at most C d⁶ B + #S.