For an auxiliary section of a surface of degree at least sixteen, all nonlinear components together contribute O(d^18 B) bounded integer points. The union of the degree-one components is not covered by this estimate.

theorem CCDN.top_form_surface_nonlinear_count : ∃ (A : ℝ), 0 < A ∧ ∀ (f : MvPolynomial (Fin 3) ℤ), HasAbsIrreducibleTopForm f → 16 ≤ f.totalDegree → ∀ (B : ℝ), 1 ≤ B → ∃ (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ), (∀ P ∈ S, IsSurfaceCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) P (δ P) ∧ 0 < δ P) ∧ (∀ (x : IntPoint 3), InBox x B → (MvPolynomial.eval x) f = 0 → ∃ P ∈ S, rationalPoint x ∈ idealZeroLocus P) ∧ ↑(∑ P ∈ S, δ P) ≤ topFormAuxiliaryConstant 1 * ↑f.totalDegree ^ (9 / 2) * B ^ (1 / ↑f.totalDegree ^ (1 / 2)) ∧ ↑(count (⋃ P ∈ {P ∈ S | 2 ≤ δ P}, idealZeroLocus P) B) ≤ A * ↑f.totalDegree ^ 18 * B ∧ ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) \ ⋃ P ∈ {P ∈ S | δ P = 1}, idealZeroLocus P) B) ≤ A * ↑f.totalDegree ^ 18 * B

The nonlinear part of the corrected large-degree surface bound, using constructed components and the curve counting theorem. The constant precedes the surface equation, its coefficients, and the box radius.