Edge deletion between explicit positional transports

A literal view of the source as a prefix plus its last edge allows deletion, followed by endpoint-fiber and reversal preserving reindexing into an actual target graph. All numerical genus obligations are discharged internally by deletion and transport. Keeping the graph parameters abstract avoids elaborating concrete dense-name construction programs inside the general surgery proof.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_deleteLastEdge_transport {S G T : Graph} {u v : ℕ} (r : S.RotationSystem) (h : S = lastEdgeGraph G u v) (e : G.Dart ≃ T.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) (he : ∀ (a : G.Dart), e a.reverse = (e a).reverse) (hS : ∀ w ∈ S.incidenceVertices, w ∈ S.vertices) (hT : ∀ w ∈ T.incidenceVertices, w ∈ T.vertices) (hr : r.NumericalGenusZero) : ((r.transport (graphEqDartEquiv h) ⋯).deleteLastEdge.transport e hv).NumericalGenusZero

A source equality, last-edge deletion and explicit target dart map preserve numerical genus. Neither endpoint name injection nor a connectedness/cofaciality hypothesis is needed. Endpoint declaration is required only on the actual source and actual target graphs.