Disjoint union of actual listed multigraphs

Even names tag the left graph and odd names tag the right graph. Declarations and indexed edges are concatenated without deduplication. The dart equivalence preserves each old end and left-then-right edge order. No scan is funded by the magnitude of a vertex name.

def Cslib.Complexity.Graph.disjointUnion (G H : Graph) : Graph

Disjoint parity-tagged copies, with all left declarations and edges before all right declarations and edges. Duplicate declarations, loops, parallel edges and points survive.

def Cslib.Complexity.Graph.disjointDartEquiv (G H : Graph) : G.Dart ⊕ H.Dart ≃ (G.disjointUnion H).Dart

The complete indexed dart sum, retaining all old edge ends in concatenation order.

theorem Cslib.Complexity.Graph.disjointDartEquiv_inl (G H : Graph) (d : G.Dart) : (G.disjointDartEquiv H) (Sum.inl d) = (⟨↑d.1, ⋯⟩, d.2)

Left indexed ends occupy the unchanged edge-list prefix.

theorem Cslib.Complexity.Graph.disjointDartEquiv_inr (G H : Graph) (d : H.Dart) : (G.disjointDartEquiv H) (Sum.inr d) = (⟨G.edges.length + ↑d.1, ⋯⟩, d.2)

Right indexed ends follow exactly the old left edge count.

theorem Cslib.Complexity.Graph.vertex_disjointDartEquiv_inl (G H : Graph) (d : G.Dart) : ((G.disjointDartEquiv H) (Sum.inl d)).vertex = 2 * d.vertex

Actual left endpoints carry the even tag, including both ends of a loop.

theorem Cslib.Complexity.Graph.vertex_disjointDartEquiv_inr (G H : Graph) (d : H.Dart) : ((G.disjointDartEquiv H) (Sum.inr d)).vertex = 2 * d.vertex + 1

Actual right endpoints carry the odd tag, irrespective of sparse binary labels.

theorem Cslib.Complexity.Graph.reverse_disjointDartEquiv (G H : Graph) (d : G.Dart ⊕ H.Dart) : (G.disjointDartEquiv H) (Sum.map Dart.reverse Dart.reverse d) = ((G.disjointDartEquiv H) d).reverse

Parity tagging retains all old edge reversals in their respective indexed blocks.

theorem Cslib.Complexity.Graph.endpoints_declared_disjointUnion (G H : Graph) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) (v : ℕ) : v ∈ (G.disjointUnion H).incidenceVertices → v ∈ (G.disjointUnion H).vertices

Endpoint declaration is inherited from the corresponding source graph.