Finite families of rational affine lines on a surface. Grouping lines by their projective direction combines the primitive spacing bound with the uniform reciprocal-height sum.

theorem CCDN.surface_line_contribution : ∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin 3) ℤ), HasAbsIrreducibleTopForm f → 3 ≤ f.totalDegree → ∀ (B : ℝ), 0 ≤ B → ∀ (s : Finset (Set (RatPoint 3))), (∀ L ∈ s, ∃ (a : RatPoint 3) (v : RatPoint 3), L = rationalAffineLine a v) → (∀ L ∈ s, L ⊆ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) → ∑ L ∈ s, ↑(count L B) ≤ C * ↑f.totalDegree ^ 6 * B + ↑s.card ∧ ↑(count (⋃ L ∈ s, L) B) ≤ C * ↑f.totalDegree ^ 6 * B + ↑s.card

Corrected CCDN Proposition 4.3.3 for a finite set of rational affine lines. Absolute irreducibility of the leading form supplies the parallel-line bound inside the proof. The constant is chosen before the surface, its degree, the radius and the family of lines.