The indexed dual of a rotation system

The dual retains every edge-list position. Its vertices are the least dart indices of all source face orbits, including singleton orbits. Its rotation is the source face successor. Declared isolated source vertices have no darts and hence contribute no dual vertex.

This is an original finite permutation construction. It does not assert geometric realization or give a native certificate compiler.

Main definitions

• Cslib.Complexity.Graph.RotationSystem.faceId: canonical least-index face name.
• Cslib.Complexity.Graph.RotationSystem.dualGraph: listed dual with the same edge positions.
• Cslib.Complexity.Graph.RotationSystem.dualRotation: the actual dual rotation.

def Cslib.Complexity.Graph.RotationSystem.faceDartIndices {G : Graph} (r : G.RotationSystem) (d : G.Dart) : Finset (Fin (2 * G.edges.length))

Finite dart indices in an actual face orbit, including its least index.

theorem Cslib.Complexity.Graph.RotationSystem.faceDartIndices_nonempty {G : Graph} (r : G.RotationSystem) (d : G.Dart) : (r.faceDartIndices d).Nonempty

Every dart belongs to its own face orbit.

def Cslib.Complexity.Graph.RotationSystem.faceId {G : Graph} (r : G.RotationSystem) (d : G.Dart) : ℕ

The least dart index in the actual face orbit, including a singleton orbit. It is computed over the finite dart universe, independently of the magnitudes of source vertex names.

theorem Cslib.Complexity.Graph.RotationSystem.faceId_spec {G : Graph} (r : G.RotationSystem) (d : G.Dart) : ∃ (e : G.Dart), e.index = r.faceId d ∧ r.faceNext.SameCycle d e ∧ r.IsFaceRepresentative e

The canonical name is attained by a least-index dart in the same actual face orbit.

theorem Cslib.Complexity.Graph.RotationSystem.faceId_eq_iff {G : Graph} (r : G.RotationSystem) (d e : G.Dart) : r.faceId d = r.faceId e ↔ r.faceNext.SameCycle d e

Canonical face names agree exactly on source face orbits.

theorem Cslib.Complexity.Graph.RotationSystem.faceId_eq_index_iff {G : Graph} (r : G.RotationSystem) (d : G.Dart) : r.faceId d = d.index ↔ r.IsFaceRepresentative d

A dart is the canonical representative exactly when its index is its face's name.

theorem Cslib.Complexity.Graph.RotationSystem.faceId_lt {G : Graph} (r : G.RotationSystem) (d : G.Dart) : r.faceId d < 2 * G.edges.length

The canonical face name is bounded by the number of darts, even for huge vertex labels.

theorem Cslib.Complexity.Graph.RotationSystem.faceId_eq_iff_faceTable {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d e : G.Dart) : r.faceId d = r.faceId e ↔ RotationCertificate.orbitBool (2 * G.edges.length) (RotationCertificate.faceTable G (RotationCertificate.ofRotation r)) d.index e.index = true

Canonical dual vertex equality is exactly the existing executable face-table orbit test. This links the abstract construction to faceTable (ofRotation r) without another face enumeration or an existentially chosen relabeling.

def Cslib.Complexity.Graph.RotationSystem.dualGraph {G : Graph} (r : G.RotationSystem) : Graph

The listed dual has one vertex per actual face and one edge per source edge occurrence. The first/second ends of edge i are the faces of darts (i,false) and (i,true).

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.dualGraph_length {G : Graph} (r : G.RotationSystem) : r.dualGraph.edges.length = G.edges.length

Dualization preserves the number of listed edges, including loops and parallel edges.

def Cslib.Complexity.Graph.RotationSystem.dualDartEquiv {G : Graph} (r : G.RotationSystem) : G.Dart ≃ r.dualGraph.Dart

Identification of source and dual darts preserves edge positions and endpoint bits.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.dualDartEquiv_reverse {G : Graph} (r : G.RotationSystem) (d : G.Dart) : r.dualDartEquiv d.reverse = (r.dualDartEquiv d).reverse

Dart reversal commutes with the source/dual identification.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_dualDartEquiv {G : Graph} (r : G.RotationSystem) (d : G.Dart) : (r.dualDartEquiv d).vertex = r.faceId d

The endpoint of a dual dart is exactly the canonical name of its source face.

theorem Cslib.Complexity.Graph.RotationSystem.dual_vertex_mem {G : Graph} (r : G.RotationSystem) (d : r.dualGraph.Dart) : d.vertex ∈ r.dualGraph.vertices

Every dual dart endpoint is declared, with no assumption on source endpoint declarations.

theorem Cslib.Complexity.Graph.RotationSystem.dualGraph_no_isolates {G : Graph} (r : G.RotationSystem) (v : ℕ) (hv : v ∈ r.dualGraph.vertices) : ∃ (d : r.dualGraph.Dart), d.vertex = v

Each declared dual vertex is incident to a dual dart. Source isolated vertices are omitted.

theorem Cslib.Complexity.Graph.RotationSystem.dualGraph_endpoints_declared {G : Graph} (r : G.RotationSystem) (v : ℕ) : v ∈ r.dualGraph.incidenceVertices → v ∈ r.dualGraph.vertices

Every endpoint in the dual's flattened incidence list is declared.

def Cslib.Complexity.Graph.RotationSystem.dualRotation {G : Graph} (r : G.RotationSystem) : r.dualGraph.RotationSystem

The dual rotation is the source face permutation, transported along the indexed dart identification. Its cycles are exactly the dual endpoint fibers.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.dualRotation_rotate {G : Graph} (r : G.RotationSystem) (d : G.Dart) : r.dualRotation.rotate (r.dualDartEquiv d) = r.dualDartEquiv (r.faceNext d)

Exact dual vertex successor: sigma_D = phi.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.dualRotation_faceNext {G : Graph} (r : G.RotationSystem) (d : G.Dart) : r.dualRotation.faceNext (r.dualDartEquiv d) = r.dualDartEquiv (r.rotate d.reverse).reverse

Exact dual face successor: phi_D = alpha sigma alpha on identified darts.

theorem Cslib.Complexity.Graph.RotationSystem.dual_sameFace_iff {G : Graph} (r : G.RotationSystem) (d e : G.Dart) : r.dualRotation.faceNext.SameCycle (r.dualDartEquiv d) (r.dualDartEquiv e) ↔ d.reverse.vertex = e.reverse.vertex

Dual faces are precisely source vertex cycles, with reversal giving the orientation identification. This includes source degree-one vertices and singleton dual face orbits.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationSystem.IncidentVertex (G : Graph) : Type

Nonempty source endpoint fibers; declared isolated vertices are deliberately absent.

noncomputable def Cslib.Complexity.Graph.RotationSystem.dualFaceVertexEquiv {G : Graph} (r : G.RotationSystem) : r.dualRotation.Face ≃ IncidentVertex G

Complete dual-face/source-vertex correspondence. It applies to every nonempty endpoint fiber, including singleton rotations, with no connectedness or genus assumption.

theorem Cslib.Complexity.Graph.RotationSystem.card_dual_faces {G : Graph} (r : G.RotationSystem) : Nat.card r.dualRotation.Face = Nat.card (IncidentVertex G)

The complete dual face count is the number of nonempty source vertex fibers.

noncomputable def Cslib.Complexity.Graph.RotationSystem.faceDualVertexEquiv {G : Graph} (r : G.RotationSystem) : r.Face ≃ { v : ℕ // v ∈ r.dualGraph.vertices }

Canonical names identify every source face with exactly one declared dual vertex.

theorem Cslib.Complexity.Graph.RotationSystem.card_dual_vertices {G : Graph} (r : G.RotationSystem) : r.dualGraph.distinctVertices.length = Nat.card r.Face

Distinct declared dual names count every source face once.