Listed cycles of a finite permutation

The edge indexed by i joins i to f i. The actual two-incidence vertex rotation and its two opposite face directions retain singleton loops and parallel positions. These graphs provide finite Boolean face potentials through the existing incidence lifting theorem; they are auxiliary listed graphs, not a replacement CSP or plane-map model.

def Cslib.Complexity.Graph.RotationSystem.permutationGraph {n : ℕ} (f : Equiv.Perm (Fin n)) : Graph

One actual listed edge from each index to its image under the finite permutation.

def Cslib.Complexity.Graph.RotationSystem.permutationEdgeEquiv {n : ℕ} (f : Equiv.Perm (Fin n)) : Fin n ≃ Fin (permutationGraph f).edges.length

Edge positions are exactly the original permutation indices.

def Cslib.Complexity.Graph.RotationSystem.permutationDartEquiv {n : ℕ} (f : Equiv.Perm (Fin n)) : Fin n × Bool ≃ (permutationGraph f).Dart

Original index/end coordinates on the actual graph.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_permutationDartEquiv {n : ℕ} (f : Equiv.Perm (Fin n)) (i : Fin n) (b : Bool) : ((permutationDartEquiv f) (i, b)).vertex = if b = true then ↑(f i) else ↑i

The first end has name i, the second name f i, including fixed-point loops.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.reverse_permutationDartEquiv {n : ℕ} (f : Equiv.Perm (Fin n)) (i : Fin n) (b : Bool) : ((permutationDartEquiv f) (i, b)).reverse = (permutationDartEquiv f) (i, !b)

Reversal keeps its original edge position.

def Cslib.Complexity.Graph.RotationSystem.permutationVertexDartEquiv {n : ℕ} (f : Equiv.Perm (Fin n)) : Fin n × Bool ≃ (permutationGraph f).Dart

Index a vertex's outgoing and incoming incidences, in that order.

def Cslib.Complexity.Graph.RotationSystem.permutationRotation {n : ℕ} (f : Equiv.Perm (Fin n)) : (permutationGraph f).RotationSystem

Every listed vertex has exactly the two indexed incidences of its permutation cycle.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_permutationDartEquiv {n : ℕ} (f : Equiv.Perm (Fin n)) (i : Fin n) (b : Bool) : (permutationRotation f).rotate ((permutationDartEquiv f) (i, b)) = (permutationDartEquiv f) (if b = true then f i else (Equiv.symm f) i, !b)

Exact directed vertex splice, in the original edge/end coordinates.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_permutationDartEquiv {n : ℕ} (f : Equiv.Perm (Fin n)) (i : Fin n) (b : Bool) : (permutationRotation f).faceNext ((permutationDartEquiv f) (i, b)) = (permutationDartEquiv f) (if b = true then (Equiv.symm f) i else f i, b)

The two face directions follow f and its inverse separately.

theorem Cslib.Complexity.Graph.RotationSystem.permutationGraph_endpoints_declared {n : ℕ} (f : Equiv.Perm (Fin n)) (v : ℕ) : v ∈ (permutationGraph f).incidenceVertices → v ∈ (permutationGraph f).vertices

All endpoints are actual declared permutation indices.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_permutationRotation {n : ℕ} (f : Equiv.Perm (Fin n)) : (permutationRotation f).NumericalGenusZero

Each permutation-cycle component has equally many vertices and indexed edges, and its two face directions are distinct. The universal matrix Euler bound supplies equality. Fixed points produce ordinary sphere loops; the empty permutation graph has no components.

theorem Cslib.Complexity.Graph.RotationSystem.sameFace_permutationDartEquiv_iff {n : ℕ} (f : Equiv.Perm (Fin n)) (i j : Fin n) (b c : Bool) : (permutationRotation f).faceNext.SameCycle ((permutationDartEquiv f) (i, b)) ((permutationDartEquiv f) (j, c)) ↔ b = c ∧ f.SameCycle i j

The complete face classes are the two oriented copies of the original permutation orbits, including fixed points.

theorem Cslib.Complexity.Graph.RotationSystem.exists_potential_of_cycleSum_zero {n : ℕ} (f : Equiv.Perm (Fin n)) (x : Fin n → Bool) (h : ∀ (i : Fin n), (∑ j : Fin n, if f.SameCycle i j then x j else 0) = 0) : ∃ (p : Fin n → Bool), ∀ (i : Fin n), x i = (p i ^^ p (f i))

A Boolean labeling with zero sum on every full finite permutation orbit is a difference of a Boolean potential at consecutive points. The proof constructs actual listed cycle graphs and discharges their numerical genus internally before invoking existing incidence lifting.