Half-open horizontal ray crossings

A segment contributes to the ray from z towards positive real infinity when its intersection with the horizontal line through z lies strictly to the right. The lower endpoint height is included and the upper endpoint height is excluded, independently of the orientation of the segment. Horizontal segments contribute nothing.

The crossing test is characterized by actual real affine parameters, including crossings at the lower endpoint. These are original finite geometric calculations. They do not assert local constancy of a closed chain's parity or construct colors on graph faces.

noncomputable def Cslib.Polygonal.horizontalIntercept (a b : ℂ) (h : ℝ) : ℝ

The real coordinate where the supporting line of a nonhorizontal segment meets height h. The formula is total; the horizontal case is excluded by RayCrosses.

def Cslib.Polygonal.RayCrosses (a b z : ℂ) : Prop

Crossing of the positive horizontal ray with the lower endpoint height included and the upper endpoint height excluded. The base point itself is excluded by a strict real coordinate comparison. Horizontal and degenerate segments never contribute.

theorem Cslib.Polygonal.not_rayCrosses_of_im_eq {a b : ℂ} (hab : a.im = b.im) (z : ℂ) : ¬RayCrosses a b z

A horizontal segment contributes no ray crossing, even at its own height.

theorem Cslib.Polygonal.horizontalIntercept_reverse {a b : ℂ} (hab : a.im ≠ b.im) (h : ℝ) : horizontalIntercept b a h = horizontalIntercept a b h

A nonhorizontal supporting line has the same intercept after reversing its ends.

theorem Cslib.Polygonal.rayCrosses_reverse (a b z : ℂ) : RayCrosses b a z ↔ RayCrosses a b z

The half-open convention depends on height, not on the order of the endpoints.

@[simp]

theorem Cslib.Polygonal.horizontalIntercept_left (a b : ℂ) : horizontalIntercept a b a.im = a.re

At the first endpoint's height, the supporting-line intercept is that endpoint.

theorem Cslib.Polygonal.horizontalIntercept_right {a b : ℂ} (hab : a.im ≠ b.im) : horizontalIntercept a b b.im = b.re

At the second endpoint's height, the supporting-line intercept is that endpoint.

theorem Cslib.Polygonal.lineMap_im (a b : ℂ) (t : ℝ) : ((AffineMap.lineMap a b) t).im = a.im + t * (b.im - a.im)

The imaginary coordinate along a real affine segment is affine in its parameter.

theorem Cslib.Polygonal.rayCrosses_iff_exists (a b z : ℂ) : RayCrosses a b z ↔ ∃ t ∈ Set.Icc 0 1, ((AffineMap.lineMap a b) t).im = z.im ∧ z.re < ((AffineMap.lineMap a b) t).re ∧ z.im < max a.im b.im

A crossing is an intersection at an actual real segment parameter. The final strict height inequality is exactly the exclusion of the upper endpoint. No generic-position or nonhorizontal assumption is hidden: horizontal segments make both sides false.

theorem Cslib.Polygonal.eventually_rayCrosses_iff (a b z : ℂ) (ha : z.im ≠ a.im) (hb : z.im ≠ b.im) (hx : z.re ≠ horizontalIntercept a b z.im) : ∀ᶠ (w : ℂ) in nhds z, RayCrosses a b w ↔ RayCrosses a b z

Away from the endpoint heights and the supporting-line intercept, the ray-crossing test is constant in a neighborhood. This is a statement about an actual open neighborhood in the real plane, rather than finitely many test points. It does not handle cancellation of jumps at the endpoint heights of a closed segment chain.

theorem Cslib.Polygonal.intercept_ne_of_not_mem_segment (a b z : ℂ) (hlo : min a.im b.im ≤ z.im) (hhi : z.im < max a.im b.im) (hz : z ∉ segment ℝ a b) : z.re ≠ horizontalIntercept a b z.im

At a height in the half-open vertical range, a base point off the actual segment cannot coincide with the segment's horizontal intercept.

theorem Cslib.Polygonal.eventually_rayCrosses_iff_of_not_mem_segment (a b z : ℂ) (ha : z.im ≠ a.im) (hb : z.im ≠ b.im) (hz : z ∉ segment ℝ a b) : ∀ᶠ (w : ℂ) in nhds z, RayCrosses a b w ↔ RayCrosses a b z

Away from the endpoint heights, avoiding the actual segment is enough for local constancy. Points on extensions of the supporting line are included.

theorem Cslib.Polygonal.eventually_rayCrosses_endpoint_jump (a b z : ℂ) (hab : a.im ≠ b.im) (hz : z.im = a.im) (hx : z.re ≠ a.re) : ∀ᶠ (w : ℂ) in nhds z, (decide (RayCrosses a b w) ^^ decide (RayCrosses a b z)) = (decide (z.re < a.re) && !decide (z.im ≤ w.im))

At an endpoint height of a nonhorizontal segment, its ray bit changes exactly when that endpoint is to the right of the base point and the observation point moves below the height. This includes either segment orientation and quantifies over a whole neighborhood. The base point differs from the endpoint, as witnessed by hx.

theorem Cslib.Polygonal.eventually_rayCrosses_jump (a b z : ℂ) (hab : a.im ≠ b.im) (hz : z ∉ segment ℝ a b) : ∀ᶠ (w : ℂ) in nhds z, (decide (RayCrosses a b w) ^^ decide (RayCrosses a b z)) = ((decide (a.im = z.im ∧ z.re < a.re) ^^ decide (b.im = z.im ∧ z.re < b.re)) && !decide (z.im ≤ w.im))

The complete local change formula for a nonhorizontal segment off its actual support. Only endpoints on the positive horizontal ray can contribute jumps; each contributes once, with its actual occurrence retained. This includes observation points at endpoint heights.

noncomputable def Cslib.Polygonal.rayParity {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x : ι → Bool) (z : ℂ) : Bool

Boolean parity of the selected indexed segments crossing the positive horizontal ray. The finite index type retains repeated geometric segments as separate occurrences.

theorem Cslib.Polygonal.rayParity_add {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x y : ι → Bool) (z : ℂ) : rayParity a b (x + y) z = (rayParity a b x z ^^ rayParity a b y z)

Segment-ray parity is linear over the Boolean ring, retaining occurrence multiplicity.

theorem Cslib.Polygonal.eventually_rayParity_eq {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x : ι → Bool) (z : ℂ) (ha : ∀ (i : ι), z.im ≠ (a i).im) (hb : ∀ (i : ι), z.im ≠ (b i).im) (hx : ∀ (i : ι), z.re ≠ horizontalIntercept (a i) (b i) z.im) : ∀ᶠ (w : ℂ) in nhds z, rayParity a b x w = rayParity a b x z

The parity of a finite arrangement is constant near any point avoiding all endpoint heights and supporting lines. No geometry or topology provider is required. Endpoint-height cancellation for even arrangements is a further statement, not a premise hidden here.