Local constancy of ray parity for even segment arrangements

For a finite indexed arrangement of nonhorizontal segments, even incidence at every actual endpoint cancels the endpoint-height jumps of horizontal-ray parity. Consequently parity is constant on a neighborhood of every point off the selected support, including points at endpoint heights. Repeated occurrences and both endpoints of each segment are counted. The weaker criterion needs only zero total endpoint jump on the observation ray; global even incidence supplies this premise. Segment-interior transport uses the same criterion after removing its observed segment.

This is an original finite parity proof. It supplies no graph face colors or right-side transport theorem.

theorem Cslib.Polygonal.sum_rayParity_endpoint_jumps_eq_zero {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x : ι → Bool) (heven : ∀ (p : ℂ), ∑ i : ι, ((if a i = p then x i else 0) + if b i = p then x i else 0) = false) (z : ℂ) : ∑ i : ι, x i * (decide ((a i).im = z.im ∧ z.re < (a i).re) + decide ((b i).im = z.im ∧ z.re < (b i).re)) = 0

The sum of the endpoint-height jumps vanishes for an even finite arrangement. All actual occurrences are retained, including coincident endpoints.

theorem Cslib.Polygonal.eventually_rayParity_eq_of_endpoint_jumps_eq_zero {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x : ι → Bool) (hheight : ∀ (i : ι), (a i).im ≠ (b i).im) (z : ℂ) (hz : ∀ (i : ι), x i = true → z ∉ segment ℝ (a i) (b i)) (hjump : ∑ i : ι, x i * (decide ((a i).im = z.im ∧ z.re < (a i).re) + decide ((b i).im = z.im ∧ z.re < (b i).re)) = 0) : ∀ᶠ (w : ℂ) in nhds z, rayParity a b x w = rayParity a b x z

Local cancellation requires only zero total endpoint jump on the observation ray. Unlike global evenness, this condition is preserved when a segment whose endpoint heights are different from the observation height is removed.

theorem Cslib.Polygonal.eventually_rayParity_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) (z : ℂ) (hz : ∀ (i : ι), x i = true → z ∉ segment ℝ (a i) (b i)) : ∀ᶠ (w : ℂ) in nhds z, rayParity a b x w = rayParity a b x z

Even incidence at each actual endpoint cancels all endpoint-height jumps. The nonhorizontal hypothesis is explicit, and the base point avoids every selected segment. No simplicity, connectedness, degree bound or general-position condition on the endpoint positions is required. In particular different endpoints may be the same point.