A coefficient-uniform linear bound for primitive affine surface polynomials of each fixed degree at least five. The argument constructs its congruence auxiliaries and curve cover.
theorem
CCDN.primitive_surface_fixed_degree_linear_bound
(d : ℕ)
(hd : 5 ≤ d)
:
∃ (C : ℝ),
0 < C ∧ ∀ (f : MvPolynomial (Fin 3) ℤ),
PrimitiveIntegerPolynomial f →
HasAbsIrreducibleTopForm f →
f.totalDegree = d →
∀ (B : ℝ), 1 ≤ B → ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ C * B
For each degree d ≥ 5, there is a constant C such that every primitive integer
surface equation of degree d with absolutely irreducible top-degree form has at most C B
integral points of height at most B on its zero set, for every B ≥ 1.