Rotation transport across equality of listed graphs

The explicit edge/end equivalence graphEqDartEquiv changes neither the generated certificate nor numerical genus. Equality elimination proves these facts without unfolding a concrete graph-construction program during subsequent transport proofs.

theorem Cslib.Complexity.Graph.RotationSystem.ofRotation_graphEqDartEquiv {G H : Graph} (r : G.RotationSystem) (h : G = H) : RotationCertificate.ofRotation (r.transport (graphEqDartEquiv h) ⋯) = RotationCertificate.ofRotation r

Equality transport retains the exact generated successor list.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_graphEqDartEquiv {G H : Graph} (r : G.RotationSystem) (h : G = H) : (r.transport (graphEqDartEquiv h) ⋯).NumericalGenusZero ↔ r.NumericalGenusZero

Equality transport preserves the actual numerical genus predicate without an endpoint-declaration premise, because the listed graphs are literally equal.