Exact generated certificates from all actual dart lookups

The canonical finite successor list is determined by its length and the successor at each indexed edge end. These original list identities allow inspection after nontrivial dart transport without evaluating an inverse chosen by a structural equivalence.

theorem Cslib.Complexity.Graph.RotationCertificate.ofRotation_eq_iff {G : Graph} (r : G.RotationSystem) (c : RotationCertificate) : ofRotation r = c ↔ c.successor.length = 2 * G.edges.length ∧ ∀ (d : G.Dart), c.successor.getD d.index 0 = (r.rotate d).index

A raw table is the exact canonical generated certificate iff it has the actual dart count and agrees with every literal successor, including the empty-graph case.