The segment arrangement underlying a polygonal embedding

The interior of each actual listed segment is disjoint from every other segment occurrence. Consecutive bends may coincide only as the shared endpoints allowed by the route parameter, and the two original ends of a loop remain distinct.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.segment_interior_disjoint {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (s j : D.SegmentIndex) (hne : j ≠ s) (t : ℝ) (ht : t ∈ Set.Ioo 0 1) : (AffineMap.lineMap (D.segmentStart s) (D.segmentFinish s)) t ∉ segment ℝ (D.segmentStart j) (D.segmentFinish j)

Distinct indexed segments in an embedding cannot meet in the open interior of either segment. The statement includes different segments on the same loop route.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.segment_endpoint_contact {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (k : D.SegmentIndex × Bool) (j : D.SegmentIndex) (hp : Polygonal.rayEndpoint D.segmentStart D.segmentFinish k ∈ segment ℝ (D.segmentStart j) (D.segmentFinish j)) : D.segmentStart j = Polygonal.rayEndpoint D.segmentStart D.segmentFinish k ∨ D.segmentFinish j = Polygonal.rayEndpoint D.segmentStart D.segmentFinish k

At any listed segment endpoint, another segment can contain the point only as one of its own endpoints. This uses the actual continuum of each segment.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segment_endpoint_eq_eval {G : Graph} (D : G.PolygonalDrawing) (s : D.SegmentIndex) (tag : Bool) : Polygonal.rayEndpoint D.segmentStart D.segmentFinish (s, tag) = (D.route s.fst).eval s.snd (if tag = true then 1 else 0)

The actual point of a segment-end occurrence is its affine endpoint parameter.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.segment_ends_at_bend {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (e : Fin G.edges.length) (i : Fin (D.route e).bends) (k : D.SegmentIndex × Bool) (hp : Polygonal.rayEndpoint D.segmentStart D.segmentFinish k = (D.route e).point i.castSucc.succ) : k = (⟨e, i.castSucc⟩, true) ∨ k = (⟨e, i.succ⟩, false)

At an internal bend, the only incident segment ends are the two consecutive occurrences of its route. This includes bends of closed loop routes.

def Cslib.Complexity.Graph.PolygonalDrawing.segmentEnd {G : Graph} (D : G.PolygonalDrawing) (d : G.Dart) : D.SegmentIndex × Bool

The segment-end occurrence corresponding to one actual graph dart.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segmentEnd_injective {G : Graph} (D : G.PolygonalDrawing) : Function.Injective D.segmentEnd

Distinct graph darts retain distinct indexed segment ends, including loop ends.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segmentEnd_endpoint {G : Graph} (D : G.PolygonalDrawing) (d : G.Dart) : Polygonal.rayEndpoint D.segmentStart D.segmentFinish (D.segmentEnd d) = D.vertex d.vertex

The segment-end point of a dart is its actual named vertex.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segmentEnd_vector {G : Graph} (D : G.PolygonalDrawing) (d : G.Dart) : Polygonal.rayEndVector D.segmentStart D.segmentFinish (D.segmentEnd d) = D.germ d

The outgoing vector at a dart's segment end is its actual drawing germ.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.segment_end_at_vertex {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) (hv : v ∈ G.vertices) (k : D.SegmentIndex × Bool) (hp : Polygonal.rayEndpoint D.segmentStart D.segmentFinish k = D.vertex v) : ∃ (d : G.Dart), d.vertex = v ∧ D.segmentEnd d = k

Every segment end at a declared vertex is an actual original graph dart there. Internal bends cannot be mistaken for vertex incidences.