Constructing vertex-fiber rotations by complete orbit counts

A vertex-preserving dart permutation maps its full orbit quotient onto the actual incident vertices. Equality of these finite cardinalities proves that every nonempty vertex fiber is one cycle. Singleton cycles are included; declared points receive no invented darts. Surgery clients must prove the count from their literal permutations and actual endpoint maps.

noncomputable def Cslib.Complexity.Graph.RotationSystem.rotateOrbitEquiv {G : Graph} (r : G.RotationSystem) : Quotient (Equiv.Perm.SameCycle.setoid r.rotate) ≃ IncidentVertex G

Every actual vertex rotation has one complete orbit per incident vertex.

def Cslib.Complexity.Graph.RotationSystem.ofOrbitCount {G : Graph} (f : Equiv.Perm G.Dart) (hs : ∀ (d : G.Dart), (f d).vertex = d.vertex) (hc : Nat.card (Quotient (Equiv.Perm.SameCycle.setoid f)) = Nat.card (IncidentVertex G)) : G.RotationSystem

Complete orbit counts suffice for the one-cycle-per-incident-vertex contract, provided that the actual successor preserves endpoints. Neither property is taken as an unchecked flag.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.ofOrbitCount_rotate {G : Graph} (f : Equiv.Perm G.Dart) (hs : ∀ (d : G.Dart), (f d).vertex = d.vertex) (hc : Nat.card (Quotient (Equiv.Perm.SameCycle.setoid f)) = Nat.card (IncidentVertex G)) : (ofOrbitCount f hs hc).rotate = f

The certified constructor retains the exact supplied successor permutation.