CCDN Corollary 4.1.4 for irreducible affine hypersurfaces in three variables. Splitting of the full equation over any field extension gives an auxiliary equation of degree at most d. The prime curve components of the resulting section have total degree at most d², giving the sharp elementary bound d²(2B+1), whatever the highest homogeneous component.
theorem
CCDN.nonabsolute_affine_auxiliary
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
{n : ℕ}
(f : MvPolynomial (Fin n) k)
(hir : Irreducible f)
(hred : ¬Irreducible ((MvPolynomial.map (algebraMap k K)) f))
:
∃ (q : MvPolynomial (Fin n) k),
q ≠ 0 ∧ q.totalDegree ≤ f.totalDegree ∧ ¬f ∣ q ∧ ∀ (x : Fin n → k), (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval x) q = 0
Linear descent of both proper factors produces a base-field auxiliary equation vanishing at every base-field zero, with degree at most d.
theorem
CCDN.finite_curve_union_count_le_box_side
(S : Finset (Ideal (CoordinatePolynomial 3)))
(d : Ideal (CoordinatePolynomial 3) → ℕ)
(hcurve : ∀ P ∈ S, P.IsPrime ∧ P.height = 2 ∧ HasAffineCurveDegree P (d P))
{B : ℝ}
(hB : 0 ≤ B)
:
A finite union of affine curves in three-space, given by height-two primes P of degree
d P, has at most (∑ P, d P) * (2 * B + 1) integral points of height at most B.