The retained part of the small-degree surface cover. Lines and nonlinear prime curves are counted together, using their common degree budget and the logarithmic cap on the retained degrees.

theorem CCDN.retained_surface_curve_union_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin 3) ℤ), HasAbsIrreducibleTopForm f → 5 ≤ f.totalDegree → ∀ (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ) (A D B : ℝ), 0 ≤ A → 0 ≤ D → 1 ≤ B → (∀ I ∈ S, IsSurfaceCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) I (δ I) ∧ 0 < δ I) → (∀ I ∈ S, ↑(δ I) ≤ D * (Real.log B + 1)) → ∑ I ∈ S, ↑(δ I) ≤ A * B ^ (1 / √↑f.totalDegree) * (Real.log B + 1) → ↑(count (⋃ I ∈ S, idealZeroLocus I) B) ≤ C * (↑f.totalDegree ^ 6 + A * (D ^ 2 * (D + 1) + 1)) * B

There is an absolute constant C such that, for an integer surface equation f of degree d ≥ 5 with absolutely irreducible top-degree form and a finite family S of curves of positive degree on the surface, each of degree at most D (log B + 1) and of total degree at most A B^(1/√d) (log B + 1), the union of the curves has at most C (d⁶ + A (D² (D + 1) + 1)) B integral points of height at most B.