Separating planar segments by a supporting line

Multiplication by a complex number followed by imaginary part is a real-linear functional. Suppose this functional, applied to displacement from the first segment's initial endpoint, vanishes on that segment and has the same strict sign at both endpoints of another. Then the segments are disjoint. This is a convenient signed half-plane test for polygonal boundaries with reentrant corners.

theorem TauCeti.disjoint_segment_of_im_mul_sub_pos (c u v w x : ℂ) (hline : (c * (v - u)).im = 0) (hw : 0 < (c * (w - u)).im) (hx : 0 < (c * (x - u)).im) : Disjoint (segment ℝ u v) (segment ℝ w x)

If a real-linear height is zero along one segment and positive at both endpoints of a second segment, the segments are disjoint.

theorem TauCeti.disjoint_segment_of_im_mul_sub_neg (c u v w x : ℂ) (hline : (c * (v - u)).im = 0) (hw : (c * (w - u)).im < 0) (hx : (c * (x - u)).im < 0) : Disjoint (segment ℝ u v) (segment ℝ w x)

The corresponding test when the second segment lies strictly on the negative side of the supporting line.

theorem TauCeti.eq_left_of_mem_segment_of_im_mul_sub_ne (c u v w x z : ℂ) (hline : (c * (v - u)).im = 0) (hw : (c * (w - u)).im = 0) (hx : (c * (x - u)).im ≠ 0) (hz₁ : z ∈ segment ℝ u v) (hz₂ : z ∈ segment ℝ w x) : z = w

A segment on a supporting line can meet a segment with one endpoint on the line and the other off the line only at the endpoint on the line.

theorem TauCeti.eq_endpoint_of_mem_segment_of_polyline_edge_of_im_mul_sub_pos {n : ℕ} (c u v : ℂ) (V : Fin (n + 2) → ℂ) (hn : 0 < n) (hline : (c * (v - u)).im = 0) (hfirst : (c * (V 0 - u)).im = 0) (hlast : (c * (V (Fin.last (n + 1)) - u)).im = 0) (hheight : ∀ (k : Fin (n + 2)), k ≠ 0 → k ≠ Fin.last (n + 1) → 0 < (c * (V k - u)).im) (i : Fin (n + 1)) (z : ℂ) (hzline : z ∈ segment ℝ u v) (hzedge : z ∈ segment ℝ (V i.castSucc) (V i.succ)) : z = V 0 ∨ z = V (Fin.last (n + 1))

If the interior vertices of a finite polyline lie strictly on one side of a supporting line and its endpoints lie on the line, an edge meets a segment on the line only at a polyline endpoint.

theorem TauCeti.eq_left_of_mem_segment_of_im_le_of_lt {u v z : ℂ} {h : ℝ} (hu : h ≤ u.im) (hv : h < v.im) (hz : z ∈ segment ℝ u v) (hzh : z.im ≤ h) : z = u

A segment with one endpoint at or above a horizontal line and the other strictly above it can meet the closed lower half-plane only at the first endpoint.