Unbounded-arity ordered incidence stars

The center has the prescribed forward cyclic order, with no degree bound. Leaves keep singleton vertex rotations. The face permutation is a doubled inverse center cycle, so a positive star has precisely one full dart face. A zero-arity star is the declared center point and retains the existing conventional-face rule.

def Cslib.Complexity.Graph.RotationSystem.starGraph (n : ℕ) : Graph

One distinct leaf per argument and one constraint center, including the arity-zero point.

def Cslib.Complexity.Graph.RotationSystem.starDartEquiv (n : ℕ) : Fin n × Bool ≃ (starGraph n).Dart

Argument/end coordinates on the actual listed star.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_starDartEquiv {n : ℕ} (i : Fin n) (b : Bool) : ((starDartEquiv n) (i, b)).vertex = if b = true then n else ↑i

The leaves use their own argument indices and the center has name n.

def Cslib.Complexity.Graph.RotationSystem.starRotor (n : ℕ) : Equiv.Perm (Fin n × Bool)

Center successor is forward argument rotation; each leaf successor is its own dart.

def Cslib.Complexity.Graph.RotationSystem.starRotation (n : ℕ) : (starGraph n).RotationSystem

Actual indexed star rotation, with one vertex cycle per endpoint fiber.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.reverse_starDartEquiv {n : ℕ} (i : Fin n) (b : Bool) : ((starDartEquiv n) (i, b)).reverse = (starDartEquiv n) (i, !b)

Reversal changes only the endpoint bit of an actual star occurrence.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_starDartEquiv {n : ℕ} (i : Fin n) (b : Bool) : (starRotation n).faceNext ((starDartEquiv n) (i, b)) = (starDartEquiv n) (if b = true then i else (Equiv.symm (finRotate n)) i, !b)

The literal face step: turn back at the center, and then return along a leaf.

theorem Cslib.Complexity.Graph.RotationSystem.sameFace_starRotation {n : ℕ} (d e : (starGraph n).Dart) : (starRotation n).faceNext.SameCycle d e

The full star face is one orbit, including the unary two-dart boundary walk.

theorem Cslib.Complexity.Graph.RotationSystem.card_faces_starRotation {n : ℕ} (hn : 0 < n) : Nat.card (starRotation n).Face = 1

A positive star has one actual dart face; the zero star has no dart face.

theorem Cslib.Complexity.Graph.RotationSystem.starGraph_endpoints_declared (n v : ℕ) : v ∈ (starGraph n).incidenceVertices → v ∈ (starGraph n).vertices

Every indexed endpoint is declared, without a bound on the arity.

theorem Cslib.Complexity.Graph.RotationSystem.starGraph_connected (n u : ℕ) : u ∈ (starGraph n).vertices → ∀ v ∈ (starGraph n).vertices, RotationCertificate.SameComponent (starGraph n) u v

All declared star vertices lie in its center's component.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_starRotation (n : ℕ) : (starRotation n).NumericalGenusZero

Ordered stars of every arity have componentwise numerical genus zero. The nullary center is a point component; positive stars use the complete doubled face orbit.