Two ordered stars on the same distinct leaves

The two centers see opposite cyclic orders on their common leaves. The second edge block lists the leaves in reverse, so both center rotations follow their literal edge-list order. This is the arbitrary-arity skeleton of an atom with its structural exterior probe. Its numerical proof counts all four-dart faces, including the unary case. At arity zero the two centers are separate declared points and there are no dart faces.

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

Two centers attached to the same indexed leaves, with the second scope reversed.

def Cslib.Complexity.Graph.RotationSystem.doubleStarEdgeEquiv (n : ℕ) : Fin n × Bool ≃ Fin (doubleStarGraph n).edges.length

A leaf and a center-block bit identify an actual edge position.

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

Leaf/block/end coordinates retain every actual edge occurrence.

theorem Cslib.Complexity.Graph.RotationSystem.val_doubleStarEdgeEquiv {n : ℕ} (i : Fin n) (b : Bool) : ↑((doubleStarEdgeEquiv n) (i, b)) = if b = true then n + ↑i.rev else ↑i

The first block is in ascending leaf order and the second in descending leaf order.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_doubleStarDartEquiv {n : ℕ} (i : Fin n) (b s : Bool) : ((doubleStarDartEquiv n) ((i, b), s)).vertex = if s = true then if b = true then n + 1 else n else ↑i

Center names are n and n+1; both variable ends use the original leaf name.

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

Leaf rotations exchange their two incidences. The first center turns forwards in leaf coordinates and the second backwards, hence forwards in its reversed scope positions.

def Cslib.Complexity.Graph.RotationSystem.doubleStarRotation (n : ℕ) : (doubleStarGraph n).RotationSystem

Actual two-center rotation, preserving the direction of both ordered scopes.

@[simp]

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

Reversal changes only the end bit.

theorem Cslib.Complexity.Graph.RotationSystem.card_faces_doubleStarRotation (n : ℕ) : Nat.card (doubleStarRotation n).Face = n

Each leaf contributes one four-dart face, with no exceptional degree bound. The nullary graph has no dart face, although its two point components have conventional faces.

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

Both centers and every leaf are declared, also at zero arity.

theorem Cslib.Complexity.Graph.RotationSystem.doubleStarGraph_connected {n : ℕ} (hn : 0 < n) (u : ℕ) : u ∈ (doubleStarGraph n).vertices → ∀ v ∈ (doubleStarGraph n).vertices, RotationCertificate.SameComponent (doubleStarGraph n) u v

At positive arity the two centers are joined through a real leaf. The nullary centers remain separate points and are deliberately excluded from this connectedness statement.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_doubleStarRotation (n : ℕ) : (doubleStarRotation n).NumericalGenusZero

The literal two-star rotation has componentwise numerical genus zero at every arity. At zero arity the conventional faces belong to the two point components, not the dart quotient.