Transport of ray parity along isolated segment interiors

The trace of ray parity on the interior of an isolated segment is constant when the arrangement has even incidence. Removing the observed segment leaves its endpoint jumps unchanged at every interior height. This gives transport without choosing a positive distance from all the other endpoint heights. Local cancellation and its even-incidence specialization are supplied by RayParityEven; this module applies that shared criterion to the arrangement with the observed segment removed.

theorem Cslib.Polygonal.not_rayCrosses_lineMap {a b : ℂ} (hab : a.im ≠ b.im) (t : ℝ) : ¬RayCrosses a b ((AffineMap.lineMap a b) t)

A point on a nonhorizontal segment never counts that same segment as a crossing: the horizontal ray excludes its base point.

theorem Cslib.Polygonal.rayParity_lineMap_eq_of_even {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x : ι → Bool) (hheight : ∀ (i : ι), (a i).im ≠ (b i).im) (heven : ∀ (p : ℂ), ∑ i : ι, ((if a i = p then x i else 0) + if b i = p then x i else 0) = false) (i : ι) (hisolated : ∀ (j : ι), j ≠ i → ∀ t ∈ Set.Ioo 0 1, (AffineMap.lineMap (a i) (b i)) t ∉ segment ℝ (a j) (b j)) {s t : ℝ} (hs : s ∈ Set.Ioo 0 1) (ht : t ∈ Set.Ioo 0 1) : rayParity a b x ((AffineMap.lineMap (a i) (b i)) s) = rayParity a b x ((AffineMap.lineMap (a i) (b i)) t)

Ray parity on the open interior of one segment is constant if no other listed segment meets that interior. The segment itself is omitted by the strict base-point convention. Endpoint jumps from other segments cancel even when their heights occur inside the observed segment's height range.