Numerical Euler bounds in edge deletion

The literal two-end deletion and complete orbit balance give an exact account of faces and endpoints that become isolated. Face-even labels extend internally across every deletion; the existing incidence lifting theorem and its algebraic converse then prove componentwise numerical genus preservation. Splitting bridges, pendant edges, loops, disconnected and point components require no provider. This is an original numerical argument, not a geometric theorem.

theorem Cslib.Complexity.Graph.RotationSystem.endpoints_declared_deleteLastEdge {G : Graph} {u v : ℕ} (hH : ∀ w ∈ (lastEdgeGraph G u v).incidenceVertices, w ∈ (lastEdgeGraph G u v).vertices) (w : ℕ) : w ∈ G.incidenceVertices → w ∈ G.vertices

Every endpoint of a retained edge was already declared before deletion.

theorem Cslib.Complexity.Graph.RotationSystem.retainedLastEdgeDart_reverse (G : Graph) (u v : ℕ) (d : G.Dart) : retainedLastEdgeDart G u v d.reverse = (retainedLastEdgeDart G u v d).reverse

The actual retained dart map commutes with reversal.

def Cslib.Complexity.Graph.RotationSystem.incidentVertexEquivDeleteLastEdge {G : Graph} {u v : ℕ} (hH : ∀ w ∈ (lastEdgeGraph G u v).incidenceVertices, w ∈ (lastEdgeGraph G u v).vertices) (hi : ∀ w ∈ G.vertices, ∃ (d : G.Dart), d.vertex = w) : IncidentVertex G ≃ IncidentVertex (lastEdgeGraph G u v)

If no declared vertex loses its last incidence, deletion preserves the actual incident vertex set. The premise is on endpoint occurrences, rather than an unchecked cardinality.

theorem Cslib.Complexity.Graph.RotationSystem.card_faces_deleteLastEdge_le {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (hH : ∀ w ∈ (lastEdgeGraph G u v).incidenceVertices, w ∈ (lastEdgeGraph G u v).vertices) (hi : ∀ w ∈ G.vertices, ∃ (d : G.Dart), d.vertex = w) : Nat.card r.Face ≤ Nat.card r.deleteLastEdge.Face + 1

Removing an edge cannot lose more than one face if every vertex retains an incident dart. The face permutation and both vertex orbit counts are those of the actual rotations.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_deleteLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (hH : ∀ w ∈ (lastEdgeGraph G u v).incidenceVertices, w ∈ (lastEdgeGraph G u v).vertices) (hr : r.NumericalGenusZero) : r.deleteLastEdge.NumericalGenusZero

Deleting an arbitrary last indexed edge preserves componentwise numerical genus zero. The internally constructed face-even extension applies also when the edge splits a component, creates isolated points, or is a loop. No connectedness or face-location premise is required.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_deleteLastEdge_of_no_edges {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (h : G.edges = []) : r.deleteLastEdge.NumericalGenusZero

If no edges remain, every declared component is a point and uses the existing conventional face. No dart or connectedness premise is required, including an empty declared list and duplicate vertex declarations.