Counting the nonlinear components of a surface section using their total Hilbert degree and the affine curve counting theorem.

theorem CCDN.count_biUnion_finset_le {n : ℕ} {ι : Type u_1} (s : Finset ι) (X : ι → Set (RatPoint n)) (B : ℝ) : count (⋃ i ∈ s, X i) B ≤ ∑ i ∈ s, count (X i) B

The number of integral points of height at most B on a finite union of sets is at most the sum of the numbers of such points on the individual sets.

theorem CCDN.nonlinear_curve_union_bound : ∃ (K : ℝ), 0 < K ∧ ∀ (s : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ) (d : ℕ), 16 ≤ d → ∀ (C B : ℝ), 0 ≤ C → 1 ≤ B → (∀ P ∈ s, P.IsPrime ∧ 2 ≤ δ P ∧ HasAffineCurveDegree P (δ P)) → ∑ P ∈ s, ↑(δ P) ≤ C * ↑d ^ (9 / 2) * B ^ (1 / √↑d) → ↑(count (⋃ P ∈ s, idealZeroLocus P) B) ≤ K * Real.exp 1 * (480 * C + 2 * C ^ 4) * ↑d ^ 18 * B

The curve counting constant is chosen before the finite family and its degree budget. This is the nonlinear-component part of the corrected surface estimate for degrees at least sixteen.