Distinct endpoint rays of an interior-disjoint segment arrangement

Actual nondegenerate segments with disjoint interiors have distinct outgoing rays at each common endpoint. The proof retains the indexed occurrences and both segment ends.

theorem Cslib.Polygonal.rayEndpoint_add_smul_endVector {ι : Type u_1} (a b : ι → ℂ) (e : ι × Bool) (t : ℝ) : rayEndpoint a b e + t • rayEndVector a b e = (AffineMap.lineMap (a e.1) (b e.1)) (if e.2 = true then 1 - t else t)

Moving along either outgoing end vector is the actual affine segment parameter, with the second end reversing the parameter.

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

Nondegenerate segments have nonzero vectors at both indexed ends.

theorem Cslib.Polygonal.rayEndVector_injective_of_interior_disjoint {ι : Type u_1} (a b : ι → ℂ) (hab : ∀ (i : ι), a i ≠ b i) (hdisjoint : ∀ (i j : ι), j ≠ i → ∀ t ∈ Set.Ioo 0 1, (AffineMap.lineMap (a i) (b i)) t ∉ segment ℝ (a j) (b j)) (k e : ι × Bool) (hp : rayEndpoint a b e = rayEndpoint a b k) (harg : turnArg (rayEndVector a b e) = turnArg (rayEndVector a b k)) : e = k

Interior disjointness forces distinct indexed outgoing rays at a common endpoint. Equal rays would give an actual common point at positive parameters less than one third.