Ray crossing at a segment germ

The local crossing contribution of a segment departing from an observation center is determined by the two height signs and their determinant. The observations use every sufficiently small positive real parameter; no discretization of the plane is used.

def Cslib.Polygonal.GermCrosses (u v : ℂ) : Prop

Germ contribution for nonhorizontal outgoing and observation vectors u and v. Equal rays contribute zero because the horizontal ray excludes its own base point.

theorem Cslib.Polygonal.eventually_rayCrosses_germ (p u v : ℂ) (hu : u.im ≠ 0) (hv : v.im ≠ 0) : ∀ᶠ (t : ℝ) in nhds 0, 0 < t → (RayCrosses p (p + u) (p + t • v) ↔ GermCrosses u v)

The half-open ray test near a genuine endpoint is the germ determinant test. The bound on the real observation parameter is constructed by continuity.

theorem Cslib.Polygonal.germCrosses_iff_turnArg {u v : ℂ} (hu : u.im ≠ 0) (hv : v.im ≠ 0) : GermCrosses u v ↔ 0 < u.im ∧ 0 < v.im ∧ turnArg u < turnArg v ∨ u.im < 0 ∧ v.im < 0 ∧ turnArg v < turnArg u

In either open half-plane, the local crossing is the strict angular interval from the cut to the observation ray, with the inequality reversed below the cut.

theorem Cslib.Polygonal.germCrosses_prefix_identity {u v : ℂ} (hu : u.im ≠ 0) (hv : v.im ≠ 0) : decide (GermCrosses u v) + decide (turnArg u = turnArg v ∧ v.im < 0) = decide (turnArg u < turnArg v) + decide (v.im < 0)

Correcting the descending observation ray itself turns the germ crossing bit into the angular prefix bit, plus one common descending-half-plane bit. Even incidence cancels that common bit when the contributions at a vertex are summed.

theorem Cslib.Polygonal.eventually_rayParity_germ {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x : ι → Bool) (hheight : ∀ (i : ι), (a i).im ≠ (b i).im) (p v : ℂ) (hv : v.im ≠ 0) (hremote : ∀ (i : ι), a i ≠ p → b i ≠ p → p.im ≠ (a i).im ∧ p.im ≠ (b i).im ∧ p ∉ segment ℝ (a i) (b i)) : ∀ᶠ (t : ℝ) in nhds 0, 0 < t → rayParity a b x (p + t • v) = rayParity a b x p + ∑ i : ι, ((if a i = p then if GermCrosses (b i - p) v then x i else 0 else 0) + if b i = p then if GermCrosses (a i - p) v then x i else 0 else 0)

The change of ray parity on leaving an arrangement endpoint along an actual ray is the sum of its incident germ contributions. Remote segments are constant near the center. Their endpoint heights and support are explicitly separated here.