Numerical genus under cofacial corner insertion

The numerical Euler argument uses the actual generated rotation and the exact face counts. The componentwise theorem includes loops, parallel edges, repeated boundary vertices and coincident corners. Untouched closed components and declared points are retained. The two selected corners are existing darts; creating an edge at a point is a separate operation.

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

Every appended edge endpoint is declared if all old endpoints were declared.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_cornerGraph_of_old {G : Graph} (h k : G.Dart) {u v : ℕ} (hc : RotationCertificate.SameComponent G u v) : RotationCertificate.SameComponent (cornerGraph h k) u v

Old edge paths remain edge paths after appending the edge.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_cornerGraph_iff {G : Graph} (h k : G.Dart) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (u v : ℕ) : RotationCertificate.SameComponent (cornerGraph h k) u v ↔ RotationCertificate.SameComponent G u v

Insertion inside one old component preserves precisely all old connected components.

theorem Cslib.Complexity.Graph.RotationSystem.componentVertexSet_cornerGraph {G : Graph} (h k : G.Dart) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (root : ℕ) : (cornerGraph h k).componentVertexSet root = G.componentVertexSet root

The declared-vertex finite set in every component is literally unchanged.

theorem Cslib.Complexity.Graph.RotationSystem.card_componentEdgeSet_cornerGraph {G : Graph} (h k : G.Dart) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (root : ℕ) : ((cornerGraph h k).componentEdgeSet root).card = (G.componentEdgeSet root).card + if RotationCertificate.SameComponent G root h.vertex then 1 else 0

The new edge contributes one indexed occurrence precisely in its selected component.

theorem Cslib.Complexity.Graph.RotationSystem.component_cornerDartEquiv {G : Graph} (h k : G.Dart) (hc : RotationCertificate.SameComponent G h.vertex k.vertex) (root : ℕ) (z : Option (Option G.Dart)) : RotationCertificate.SameComponent (cornerGraph h k) root ((cornerDartEquiv h k).symm z).vertex ↔ Equiv.Perm.SelectedOrbits.extendedPredicate (fun (d : G.Dart) => RotationCertificate.SameComponent G root d.vertex) (RotationCertificate.SameComponent G root h.vertex) z

The actual component selection agrees with the old dart selection extended to the two new edge ends. No injectivity of vertices or boundary labels is used.

theorem Cslib.Complexity.Graph.RotationSystem.card_componentFace_insertEdge {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (h k : G.Dart) (hf : r.faceNext.SameCycle h k) (root : ℕ) : Nat.card ((r.insertEdge h k).ComponentFace root) = Nat.card (r.ComponentFace root) + if RotationCertificate.SameComponent G root h.vertex then 1 else 0

Exact component face count for cofacial insertion. Only the selected component gains a face; every other component retains its full face quotient.

theorem Cslib.Complexity.Graph.RotationSystem.exists_oldCornerVertex {G : Graph} (h k : G.Dart) (d : (cornerGraph h k).Dart) : ∃ (a : G.Dart), d.vertex = a.vertex

Every new dart vertex is an old dart vertex. This uses occurrence corners, so distinct visits to a repeated vertex are retained and never require injective boundary labels.

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

Insertion at cofacial existing corners preserves componentwise numerical genus zero. Disconnected closed components and declared point components remain in the same predicate; there is no connectedness, distinct-vertex or distinct-corner hypothesis.