Directions of rational affine lines on a surface. Lines with two bounded integer points have a bounded projective direction and a spacing bound expressed using its representative-independent projective height.

theorem CCDN.eval_affineLinePolynomial {K : Type u_1} {σ : Type u_2} [Field K] (a v : σ → K) (f : MvPolynomial σ K) (t : K) : Polynomial.eval t ((affineLinePolynomial a v) f) = (MvPolynomial.eval (a + t • v)) f

Evaluating the restriction affineLinePolynomial a v f of f to the line through a with direction v at t gives the value of f at a + t • v.

theorem CCDN.surface_line_projective_direction {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (L : Set (RatPoint (n + 1))) (hL : ∃ (a : RatPoint (n + 1)) (v : RatPoint (n + 1)), L = rationalAffineLine a v) (hLf : L ⊆ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) {B : ℝ} (hB : 0 ≤ B) (hcount : 1 < count L B) : ∃ p ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) ((MvPolynomial.homogeneousComponent f.totalDegree) f)), 0 < Projectivization.mulHeight p ∧ Projectivization.mulHeight p ≤ 2 * B ∧ (∃ (a : RatPoint (n + 1)), L = rationalAffineLine a (Projectivization.rep p)) ∧ ↑(count L B) ≤ 4 * B / Projectivization.mulHeight p

A line with more than one bounded integer point has a projective direction on the leading form. Its integer point count is bounded using the height of that projective point, independently of all chosen representatives.