A transverse plane injects distinct parallel lines on a surface into the common zeros of two proper plane equations. The second equation will be the directional derivative.
theorem
CCDN.surface_parallel_lines_card_le
(f : MvPolynomial (Fin 3) ℤ)
(hir : HasAbsIrreducibleTopForm f)
(hd : 2 ≤ f.totalDegree)
(v : RatPoint 3)
(hv : v ≠ 0)
(S : Finset (Set (RatPoint 3)))
(hlines : ∀ L ∈ S, ∃ (a : RatPoint 3), L = rationalAffineLine a v)
(hSf : ∀ L ∈ S, L ⊆ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f))
:
A surface with absolutely irreducible top form has at most d(d-1) distinct lines in any prescribed nonzero rational direction. The directional derivative and the transverse plane are constructed inside the proof.