Exact certificates under positional dart transport

A dart equivalence retaining each binary edge/end index keeps the generated successor list literally unchanged. Vertex names and declared isolated points need not coincide. These original list identities connect dense incidence-name transport to computed certificate programs, without replacing either table by an existential certificate.

theorem Cslib.Complexity.Graph.RotationSystem.getD_ofRotation_transport {G H : Graph} (r : G.RotationSystem) (e : G.Dart ≃ H.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) (hi : ∀ (a : G.Dart), (e a).index = a.index) (d : G.Dart) : (RotationCertificate.ofRotation (r.transport e hv)).successor.getD d.index 0 = (r.rotate d).index

Position-preserving transport retains every literal successor-table lookup.

theorem Cslib.Complexity.Graph.RotationSystem.ofRotation_transport {G H : Graph} (r : G.RotationSystem) (e : G.Dart ≃ H.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) (hi : ∀ (a : G.Dart), (e a).index = a.index) : RotationCertificate.ofRotation (r.transport e hv) = RotationCertificate.ofRotation r

The complete generated certificate is unchanged by actual edge/end position transport.

theorem Cslib.Complexity.Graph.RotationCertificate.ofRotation_decode {G : Graph} {c : RotationCertificate} (h : verifyRotation G c = true) : ofRotation (decode G c h) = c

Decoding an accepted raw table and encoding its actual rotation returns that very table, including empty tables. Acceptance supplies the exact list length internally.