Numerical genus under arbitrary nonloop contraction

The literal incoming/outgoing face swaps permit extension of every retained face-even label with zero on the contracted edge. Vertex-spin lifting then descends through the actual endpoint identification. This original algebraic proof uses neither a bridge nor a cofacial hypothesis and includes empty residual dart sets and isolated declarations. It concerns the existing componentwise numerical predicate, without a geometric claim.

theorem Cslib.Complexity.Graph.RotationSystem.exists_faceEven_extension_contractLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (x : Fin (contractLastEdgeGraph G u v).edges.length → Bool) (hx : (r.contractLastEdge huv).FaceEven x) : ∃ (y : Fin (lastEdgeGraph G u v).edges.length → Bool), r.FaceEven y ∧ y (lastEdgeDart G u v false).1 = false ∧ ∀ (d : (contractLastEdgeGraph G u v).Dart), y (((contractLastEdgeDartEquiv G u v).trans (lastEdgeDartEquiv (contractLastEdgeGraph G u v) v v)).symm (some (some d))).1 = x d.1

Face-even labels extend across directed nonloop contraction with zero on the selected edge and the original labels on all retained indexed occurrences.

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

All retained endpoints remain declared after contracting an actual nonloop edge.

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

Contracting any actual indexed nonloop edge preserves componentwise numerical genus zero. No bridge, cofacial, connectedness or face-even lifting provider is a premise. The point convention is handled by the existing algebraic characterization, without new darts.