Predecessors in accepted raw successor tables

The predecessor of an actual dart is computed by finding its index in the supplied successor list. The scan is funded by that list and never by a binary entry. These original identities connect inverse rotations used in proofs to literal finite certificate programs.

theorem Cslib.Complexity.Graph.RotationCertificate.idxOf_ofRotation {G : Graph} (r : G.RotationSystem) (d : G.Dart) : List.idxOf d.index (ofRotation r).successor = ((Equiv.symm r.rotate) d).index

The inverse of a supplied abstract rotation is read by one positional search in its canonical table. This includes singleton vertex cycles and requires an actual dart.