Extending face-even labels across an edge deletion

The actual deleted rotation supplies a potential on its face darts. Extend that potential over both removed points with zero differences, then undo the literal face-successor swap. The two restored edge ends receive the same bit. This works for bridge splits, pendant endpoints, loops, disconnected components and empty residual dart sets. No face-location, connectedness, endpoint-declaration or genus premise is required for the parity extension.

theorem Cslib.Complexity.Graph.RotationSystem.exists_faceEven_extension_deleteLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (x : Fin G.edges.length → Bool) (hx : r.deleteLastEdge.FaceEven x) : ∃ (y : Fin (lastEdgeGraph G u v).edges.length → Bool), r.FaceEven y ∧ ∀ (i : Fin G.edges.length), y (retainedLastEdgeDart G u v (i, false)).1 = x i

Every face-even labeling of the actual deleted graph extends to a face-even labeling of the original graph, retaining every old edge position. The bit on the removed edge is constructed from face-dart potentials; no lifting or embedding provider is a premise.