Distinct outgoing geometric rays in a polygonal embedding #
Distinct incident darts of a genuine polygonal embedding have distinct outgoing ray directions. The proof constructs a small common point when the arguments are equal, then uses the actual segment contact conditions. The same-edge case treats the two ends of a loop using route simplicity. There is no degree bound or local-disk assumption.
Main results #
theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.directions_injective {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (a b : G.Dart) (hv : a.vertex = b.vertex) (harg : D.direction a = D.direction b) :
A polygonal embedding has different outgoing rays at distinct incident darts, including the two ends of a loop. This follows from segment geometry, not from rotation data.