Component and face counts for vertex identification

These facts use the literal successor swap and endpoint update of mergeVertices. The cofacial premise is needed for the face-splitting count; distinct endpoint names are needed for the two old vertex cycles to merge. Unchanged components retain their indexed faces.

theorem Cslib.Complexity.Graph.RotationSystem.mergeGraph_endpoints_declared {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (v : ℕ) : v ∈ (mergeGraph h k).incidenceVertices → v ∈ (mergeGraph h k).vertices

Original declared endpoints remain declared under the actual name update.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_mergeGraph_iff {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (a b : G.Dart) : RotationCertificate.SameComponent (mergeGraph h k) ((mergeDartEquiv h k) a).vertex ((mergeDartEquiv h k) b).vertex ↔ RotationCertificate.SameComponent G a.vertex b.vertex

Identifying two vertices already in one old component preserves exactly its edge components. This statement uses actual old and new dart endpoints, not an injective name map.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_mergeVertices {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) (d : G.Dart) : (r.mergeVertices h k hk).faceNext ((mergeDartEquiv h k) d) = (mergeDartEquiv h k) ((Equiv.swap h k * r.faceNext) d)

Literal incoming-face swap caused by the outgoing vertex-corner swap.

theorem Cslib.Complexity.Graph.RotationSystem.card_componentFace_mergeVertices {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) (hf : r.faceNext.SameCycle h k) (a : G.Dart) : Nat.card ((r.mergeVertices h k hk).ComponentFace ((mergeDartEquiv h k) a).vertex) = Nat.card (r.ComponentFace a.vertex) + if RotationCertificate.SameComponent G a.vertex h.vertex then 1 else 0

A cofacial identification adds one actual face in its component, retaining every other component's face quotient. The selected corners are distinct vertices but may revisit a face.

theorem Cslib.Complexity.Graph.RotationSystem.componentVertexSet_mergeGraph {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (a : G.Dart) : (mergeGraph h k).componentVertexSet ((mergeDartEquiv h k) a).vertex = Finset.image (Function.update id k.vertex h.vertex) (G.componentVertexSet a.vertex)

The actual component vertex set is the image of its old set under the one-name update.

theorem Cslib.Complexity.Graph.RotationSystem.card_componentVertexSet_mergeGraph {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (hk : h.vertex ≠ k.vertex) (a : G.Dart) : (((mergeGraph h k).componentVertexSet ((mergeDartEquiv h k) a).vertex).card + if RotationCertificate.SameComponent G a.vertex h.vertex then 1 else 0) = (G.componentVertexSet a.vertex).card

The selected component loses exactly the second old vertex name. Other components retain all their distinct declared names, including declared points.

theorem Cslib.Complexity.Graph.RotationSystem.card_componentEdgeSet_mergeGraph {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (a : G.Dart) : ((mergeGraph h k).componentEdgeSet ((mergeDartEquiv h k) a).vertex).card = (G.componentEdgeSet a.vertex).card

No indexed edge occurrence is removed or identified by the vertex-name update.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_mergeVertices {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hr : r.NumericalGenusZero) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) (hf : r.faceNext.SameCycle h k) : (r.mergeVertices h k hk).NumericalGenusZero

Identifying two distinct incident vertices at cofacial corners preserves the existing componentwise numerical genus-zero predicate. Closed and point components outside the selected component retain their old counts. No injective map on boundary variable labels is assumed.