The corrected large-degree surface bound. The auxiliary section's nonlinear curves and its degree-one components together account for every bounded integer zero of the original surface.

def CCDN.topFormSurfaceThreshold : ℕ

The degree threshold of the large-degree surface bound affine_surface_count_large_degree. It comes from surface_inverse_sqrt_le_quarter: 1 / √d ≤ 1 / 4 once 16 ≤ d.

Equations

• CCDN.topFormSurfaceThreshold = 16

theorem CCDN.affine_surface_count_large_degree : ∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin 3) ℤ), HasAbsIrreducibleTopForm f → topFormSurfaceThreshold ≤ f.totalDegree → ∀ (B : ℝ), 1 ≤ B → ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ C * ↑f.totalDegree ^ 18 * B

Corrected CCDN Proposition 4.3.4 for degrees at least sixteen and an absolutely irreducible highest homogeneous part. The positive constant is chosen before the integer polynomial and the real box radius.