The uniform surface auxiliary gives a finite curve cover of all bounded integer zeros, with total curve degree O(d^(9/2) B^(1/sqrt d)).

theorem CCDN.top_form_surface_curve_components (f : MvPolynomial (Fin 3) ℤ) (hir : HasAbsIrreducibleTopForm f) {B : ℝ} (hB : 1 ≤ B) : ∃ (g : MvPolynomial (Fin 3) ℤ), g ≠ 0 ∧ ¬(MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) g ∧ ↑g.totalDegree ≤ topFormAuxiliaryConstant 1 * ↑f.totalDegree ^ (7 / 2) * B ^ (1 / ↑f.totalDegree ^ (1 / 2)) ∧ (∀ (x : IntPoint 3), InBox x B → (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval x) g = 0) ∧ ∃ (S : Finset (Ideal (CoordinatePolynomial 3))) (d : Ideal (CoordinatePolynomial 3) → ℕ), (∀ P ∈ S, IsSectionCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) ((MvPolynomial.map (Int.castRingHom ℚ)) g) P (d P)) ∧ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) ∩ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) g) = ⋃ P ∈ S, idealZeroLocus P ∧ ↑(∑ P ∈ S, d P) ≤ topFormAuxiliaryConstant 1 * ↑f.totalDegree ^ (9 / 2) * B ^ (1 / ↑f.totalDegree ^ (1 / 2)) ∧ (∀ P ∈ S, (polynomialSectionIdeal ((MvPolynomial.map (Int.castRingHom ℚ)) f) ((MvPolynomial.map (Int.castRingHom ℚ)) g)).IsMinimalPrime P) ∧ ∀ (x : IntPoint 3), InBox x B → (MvPolynomial.eval x) f = 0 → ∃ P ∈ S, rationalPoint x ∈ idealZeroLocus P

An absolutely irreducible top form supplies the auxiliary equation, the rational curve components, and their total degree bound. The component cover is exact on the auxiliary section and covers every original integer zero in the specified box.