Executable boundary restriction across one actual edge deletion

The boundary's list-funded first-return program gives exactly the certificate of the generic directed last-edge deletion. Permutation injectivity bounds each retained first return by three steps, including loops, cutvertices and empty retained dart sets. Thus the numerical genus theorem applies to this literal computed table, not an assumed embedding. This original program-correctness lemma is a prerequisite for actual-body port projection.

theorem Cslib.Complexity.CSP.OrderedBoundary.getD_restrictPrefix_deleteLastEdge {G : Graph} {u v : ℕ} (r : (Graph.RotationSystem.lastEdgeGraph G u v).RotationSystem) (d : G.Dart) : (restrictPrefix (2 * G.edges.length) (Graph.RotationCertificate.ofRotation r)).successor.getD d.index 0 = (r.deleteLastEdge.rotate d).index

The bounded boundary scan reads the exact directed successor after deleting the last two actual edge ends. A retained dart needs at most three list-funded successor steps.

theorem Cslib.Complexity.CSP.OrderedBoundary.restrictPrefix_ofRotation_deleteLastEdge {G : Graph} {u v : ℕ} (r : (Graph.RotationSystem.lastEdgeGraph G u v).RotationSystem) : restrictPrefix (2 * G.edges.length) (Graph.RotationCertificate.ofRotation r) = Graph.RotationCertificate.ofRotation r.deleteLastEdge

Exact generated certificates agree, including the empty retained table. The scan's clock is the original certificate length, independent of binary labels and table values.

theorem Cslib.Complexity.CSP.OrderedBoundary.verifyGenusZero_restrictPrefix_deleteLastEdge {G : Graph} {u v : ℕ} (r : (Graph.RotationSystem.lastEdgeGraph G u v).RotationSystem) (hH : ∀ w ∈ (Graph.RotationSystem.lastEdgeGraph G u v).incidenceVertices, w ∈ (Graph.RotationSystem.lastEdgeGraph G u v).vertices) (hr : r.NumericalGenusZero) : Graph.RotationCertificate.verifyGenusZero G (restrictPrefix (2 * G.edges.length) (Graph.RotationCertificate.ofRotation r)) = true

The actual computed restriction passes the full numerical rotation checker. Source endpoint declaration and numerical genus suffice, including bridge splits and points.