Polygonal drawings of listed multigraphs

Each listed edge occurrence has its own finite polygonal route in the real plane ℂ. Both ends of a loop remain distinct route parameters. Repeated declarations of the same natural number name the same point; only distinct declared names must have distinct points. There is no constraint on undeclared names and no degree bound.

Embedding is expressed entirely by actual real segment intersections and route parameters. It excludes self-intersections, visits to unrelated vertices and intersections of different edge interiors. It does not contain a rotation, numerical genus or a drawing provider.

Main definitions

• Cslib.Complexity.Graph.PolygonalDrawing: coordinates and finite edge routes.
• Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding: genuine nonintersection conditions.

structure Cslib.Complexity.Graph.PolygonalDrawing (G : Graph) : Type

An actual finite polygonal drawing of the existing indexed listed graph. The endpoint equations hold even before requiring the endpoints to be among the declared names.

• vertex : ℕ → ℂ

  The point of each vertex name; undeclared names have no geometric restrictions.

• route : Fin G.edges.length → Polygonal.Route

  One route per listed edge occurrence, without identifying equal edge pairs.

• endpoint_eq (e : Fin G.edges.length) (b : Bool) : (self.route e).endpoint b = self.vertex (Dart.vertex (e, b))

  The two route ends are the corresponding named graph endpoints.

def Cslib.Complexity.Graph.PolygonalDrawing.germ {G : Graph} (D : G.PolygonalDrawing) (d : G.Dart) : ℂ

An actual outgoing end-segment vector, with both germs retained at a loop.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.direction {G : Graph} (D : G.PolygonalDrawing) (d : G.Dart) : Real.Angle

The actual direction of an outgoing segment in the oriented real plane.

structure Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding {G : Graph} (D : G.PolygonalDrawing) : Prop

Geometric embedding of the indexed multigraph. Every intersection below is tested at arbitrary real parameters of actual straight segments. Endpoint closure of an individual loop is permitted by simple; different edge routes may meet only at common named ends.

• vertices_injective : Set.InjOn D.vertex {v : ℕ | v ∈ G.vertices}

  Distinct declared names, including isolates, have distinct points.

• simple (e : Fin G.edges.length) : (D.route e).IsSimple

  Each route is simple except for its intended loop closure.

• vertex_contacts (e : Fin G.edges.length) (i : Fin (D.route e).segments) (t : ℝ) : t ∈ Set.Icc 0 1 → ∀ v ∈ G.vertices, (D.route e).eval i t = D.vertex v → ∃ (b : Bool), (D.route e).AtEnd i t b ∧ Dart.vertex (e, b) = v

  A declared vertex on an edge route must occur at the corresponding original end.

• edge_contacts (e f : Fin G.edges.length) : e ≠ f → ∀ (i : Fin (D.route e).segments) (j : Fin (D.route f).segments) (s t : ℝ), s ∈ Set.Icc 0 1 → t ∈ Set.Icc 0 1 → (D.route e).eval i s = (D.route f).eval j t → ∃ (b : Bool) (c : Bool), (D.route e).AtEnd i s b ∧ (D.route f).AtEnd j t c ∧ Dart.vertex (e, b) = Dart.vertex (f, c)

  Different indexed edge occurrences intersect only at common original endpoints.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.germ_ne_zero {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (d : G.Dart) : D.germ d ≠ 0

A geometric embedding has nonzero outgoing end segments.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.vertex_ne {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) {u v : ℕ} (hu : u ∈ G.vertices) (hv : v ∈ G.vertices) (huv : u ≠ v) : D.vertex u ≠ D.vertex v

Declared isolated vertices are separated just like all other distinct declared names.