Documentation

LeanPool.CCDN.Surface.DirectionSum

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.