The reciprocal heights of distinct rational projective points on a plane curve of degree at least three have a uniform, coefficient-independent sum. Geometric height bands turn the proved projective point count into the weighted estimate used for surface-line directions.
theorem
CCDN.integer_projective_plane_reciprocal_height_sum :
∃ (C : ℝ),
0 < C ∧ ∀ (d : ℕ),
3 ≤ d →
∀ (F : MvPolynomial (Fin 3) ℤ),
F.IsHomogeneous d →
AbsolutelyIrreducible F →
∀ (s : Finset (ProjectivePoint 2)),
(∀ x ∈ s, x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) F)) →
∑ x ∈ s, 1 / Projectivization.mulHeight x ≤ C * ↑d ^ 4
There is an absolute constant C such that, for every absolutely irreducible integer
homogeneous polynomial F of degree d ≥ 3 in three variables, the sum of the reciprocal
multiplicative heights of any finite set of rational points of the plane curve F = 0 is at
most C d⁴; no primitivity or coefficient-height hypothesis is needed.