Raw numerical certificates under isolated-point declaration changes

With every incident endpoint declared on both graphs, changing only the declaration list retains the exact raw numerical checker result. Extra or missing isolated points satisfy the existing conventional Euler equation separately; they need no darts. This extends the membership-preserving declaration transport to raw certificates and arbitrary point components. It asserts no geometric-planarity equivalence.

theorem Cslib.Complexity.Graph.RotationCertificate.verifyGenusZero_redeclare (vertices newVertices : List ℕ) (edges : List (ℕ × ℕ)) (hG : ∀ v ∈ { vertices := vertices, edges := edges }.incidenceVertices, v ∈ vertices) (hH : ∀ v ∈ { vertices := newVertices, edges := edges }.incidenceVertices, v ∈ newVertices) (c : RotationCertificate) : verifyGenusZero { vertices := newVertices, edges := edges } c = verifyGenusZero { vertices := vertices, edges := edges } c

Declaring different isolated points, or repeating declarations, retains the exact raw numerical-checker result when all actual edge endpoints are declared on both sides.

theorem Cslib.Complexity.Graph.RotationCertificate.verifyGenusZero_eq_of_edges_eq {G H : Graph} (he : G.edges = H.edges) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) (c : RotationCertificate) : verifyGenusZero H c = verifyGenusZero G c

Equal indexed edge lists retain the exact raw numerical result under any valid endpoint declarations. Vertex declarations may differ at point components or contain duplicates.