Angular prefix colors at the endpoints of a segment arrangement

An endpoint color adds the clockwise-side angular prefix to the horizontal-ray parity at the center. Even incidence removes the dependence on the auxiliary horizontal cut. The endpoints remain indexed separately throughout.

def Cslib.Polygonal.rayEndpoint {ι : Type u_1} (a b : ι → ℂ) (e : ι × Bool) : ℂ

An endpoint occurrence of a listed segment; false is its first endpoint.

def Cslib.Polygonal.rayEndVector {ι : Type u_1} (a b : ι → ℂ) (e : ι × Bool) : ℂ

The actual vector departing from one indexed endpoint of a segment.

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

Angular prefix value used for the color immediately clockwise from v at p. The sum ranges over every actual incident segment end; the theorems below identify it with the geometric trace under their explicit arrangement hypotheses.

theorem Cslib.Polygonal.rayEndVector_im_ne_zero {ι : Type u_1} (a b : ι → ℂ) (hheight : ∀ (i : ι), (a i).im ≠ (b i).im) (e : ι × Bool) : (rayEndVector a b e).im ≠ 0

Nonhorizontal segments have nonhorizontal vectors at both separately indexed ends.

theorem Cslib.Polygonal.eventually_rayParity_rightGerm {ι : 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) (k : ι × Bool) (hremote : ∀ (i : ι), a i ≠ rayEndpoint a b k → b i ≠ rayEndpoint a b k → (rayEndpoint a b k).im ≠ (a i).im ∧ (rayEndpoint a b k).im ≠ (b i).im ∧ rayEndpoint a b k ∉ segment ℝ (a i) (b i)) (hdistinct : ∀ (e : ι × Bool), rayEndpoint a b e = rayEndpoint a b k → turnArg (rayEndVector a b e) = turnArg (rayEndVector a b k) → e = k) : ∀ᶠ (t : ℝ) in nhds 0, 0 < t → (rayParity a b x (rayEndpoint a b k + t • rayEndVector a b k) + if (rayEndVector a b k).im < 0 then x k.1 else 0) = rayGermColor a b x (rayEndpoint a b k) (rayEndVector a b k)

The angular prefix color is the actual right-hand trace on the selected outgoing segment. Distinct incident rays, separation of remote endpoints and segments, and even incidence are geometric hypotheses on the finite arrangement.

theorem Cslib.Polygonal.rayGermColor_ends {ι : 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)) (hremote : ∀ (k : ι × Bool) (j : ι), a j ≠ rayEndpoint a b k → b j ≠ rayEndpoint a b k → (rayEndpoint a b k).im ≠ (a j).im ∧ (rayEndpoint a b k).im ≠ (b j).im ∧ rayEndpoint a b k ∉ segment ℝ (a j) (b j)) (hdistinct : ∀ (k e : ι × Bool), rayEndpoint a b e = rayEndpoint a b k → turnArg (rayEndVector a b e) = turnArg (rayEndVector a b k) → e = k) : rayGermColor a b x (a i) (b i - a i) + rayGermColor a b x (b i) (a i - b i) = x i

Endpoint prefix colors on the opposite sides of a segment differ by its label. All parameters are real and the open segment is isolated from every other occurrence. The local hypotheses concern the actual finite arrangement, without any face data.

theorem Cslib.Polygonal.rayGermColor_adjacent {ι : Type u_1} [Fintype ι] (a b : ι → ℂ) (x : ι → Bool) (hheight : ∀ (i : ι), (a i).im ≠ (b i).im) (p : ℂ) (heven : ∑ i : ι, ((if a i = p then x i else 0) + if b i = p then x i else 0) = false) (k l : ι × Bool) (hk : rayEndpoint a b k = p) (hl : rayEndpoint a b l = p) (hkl : k ≠ l) (hinj : ∀ (e f : ι × Bool), rayEndpoint a b e = p → rayEndpoint a b f = p → turnArg (rayEndVector a b e) = turnArg (rayEndVector a b f) → e = f) (hgap : ∀ (e : ι × Bool), rayEndpoint a b e = p → e ≠ k → e ≠ l → ¬sbtw ↑(rayEndVector a b k).arg ↑(rayEndVector a b e).arg ↑(rayEndVector a b l).arg) : rayGermColor a b x p (rayEndVector a b k) + rayGermColor a b x p (rayEndVector a b l) = x k.1

Angular prefix colors on the two sides of an empty counterclockwise sector differ by the label of its first ray. Both endpoint occurrences and arbitrary degree are retained.