Dart invariants and existing graph components

Adjacency is witnessed by a listed edge occurrence. Vertex and edge-reversal invariants are constant on existing declared-vertex components. Point components have no darts.

theorem Cslib.Complexity.Graph.Dart.exists_of_adj {G : Graph} {u v : ℕ} (h : G.toSimpleGraph.Adj u v) : ∃ (d : G.Dart), d.vertex = u ∧ d.reverse.vertex = v

A simple-graph adjacency is witnessed by an oriented listed edge occurrence.

theorem Cslib.Complexity.Graph.Dart.eq_of_sameComponent {G : Graph} {β : Sort u_1} (f : G.Dart → β) (hv : ∀ (d e : G.Dart), d.vertex = e.vertex → f d = f e) (ha : ∀ (d : G.Dart), f d = f d.reverse) {d e : G.Dart} (h : RotationCertificate.SameComponent G d.vertex e.vertex) : f d = f e

Vertex invariance and reversal invariance imply constancy on existing edge components. Only finite listed edge witnesses are used; the ambient natural-number universe need not be finite. The component hypothesis already includes endpoint declarations.

theorem Cslib.Complexity.Graph.Dart.exists_of_sameComponent {G : Graph} (d : G.Dart) (v : ℕ) (h : RotationCertificate.SameComponent G d.vertex v) : ∃ (e : G.Dart), e.vertex = v

Every vertex in an edge component has an incident dart. This does not invent a dart for a declared isolated point.