Finite sets counted by componentwise numerical Euler

The vertex universe is the set of declared names, edge indices are list positions, and faces use the existing least-index representative predicate. These finite sets make the existing certificate counts available to finite-dimensional arguments.

Main results

• Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_iff_component_cards: finite counts.
• Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_dual_iff: numerical duality.

noncomputable def Cslib.Complexity.Graph.componentVertexSet (G : Graph) (root : ℕ) : Finset ℕ

Distinct declared vertex names in the existing component of root.

noncomputable def Cslib.Complexity.Graph.componentEdgeSet (G : Graph) (root : ℕ) : Finset (Fin G.edges.length)

Listed edge positions whose first endpoint belongs to root's existing component.

theorem Cslib.Complexity.Graph.mem_componentVertexSet_dart {G : Graph} (root : ℕ) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : d.vertex ∈ G.componentVertexSet root ↔ RotationCertificate.SameComponent G root d.vertex

Membership for an actual dart reduces to the existing component relation.

theorem Cslib.Complexity.Graph.mem_componentEdgeSet_iff {G : Graph} (root : ℕ) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (i : Fin G.edges.length) (b : Bool) : i ∈ G.componentEdgeSet root ↔ Dart.vertex (i, b) ∈ G.componentVertexSet root

Either indexed endpoint identifies the same set of listed component edges.

theorem Cslib.Complexity.Graph.card_componentVertexSet (G : Graph) (root : ℕ) : (G.componentVertexSet root).card = List.countP (fun (v : ℕ) => decide (RotationCertificate.SameComponent G root v)) G.distinctVertices

Component vertices are counted by distinct names, independently of duplicate declarations.

theorem Cslib.Complexity.Graph.card_componentEdgeSet (G : Graph) (root : ℕ) : (G.componentEdgeSet root).card = List.countP (fun (edge : ℕ × ℕ) => decide (RotationCertificate.SameComponent G root edge.1)) G.edges

Counting indexed component edges agrees with the existing edge-list occurrence count.

noncomputable def Cslib.Complexity.Graph.RotationSystem.componentFaceIndices {G : Graph} (r : G.RotationSystem) (root : ℕ) : Finset (Fin (2 * G.edges.length))

Exactly one indexed dart per actual face in the chosen edge component.

theorem Cslib.Complexity.Graph.RotationSystem.card_componentFaceIndices {G : Graph} (r : G.RotationSystem) (root : ℕ) : (r.componentFaceIndices root).card = List.countP (fun (i : Fin (2 * G.edges.length)) => decide (RotationCertificate.SameComponent G root ((Dart.indexEquiv G).symm i).vertex ∧ r.IsFaceRepresentative ((Dart.indexEquiv G).symm i))) (List.finRange (2 * G.edges.length))

The finite face set is precisely the face count in NumericalGenusZero.

noncomputable def Cslib.Complexity.Graph.RotationSystem.componentFaceDualVertexEquiv {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : ↥(r.componentFaceIndices d.vertex) ≃ ↥(r.dualGraph.componentVertexSet (r.dualDartEquiv d).vertex)

Source face representatives and canonical dual vertex names agree in each edge component.

theorem Cslib.Complexity.Graph.RotationSystem.card_component_faces_eq_dual_vertices {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : (r.componentFaceIndices d.vertex).card = (r.dualGraph.componentVertexSet (r.dualDartEquiv d).vertex).card

Componentwise face counts equal componentwise declared dual vertex counts.

noncomputable def Cslib.Complexity.Graph.RotationSystem.componentEdgeDualEquiv {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : ↥(G.componentEdgeSet d.vertex) ≃ ↥(r.dualGraph.componentEdgeSet (r.dualDartEquiv d).vertex)

Edge positions in corresponding source and dual components are identified explicitly.

theorem Cslib.Complexity.Graph.RotationSystem.card_component_edges_eq_dual {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : (G.componentEdgeSet d.vertex).card = (r.dualGraph.componentEdgeSet (r.dualDartEquiv d).vertex).card

Corresponding components retain every listed edge occurrence.

noncomputable def Cslib.Complexity.Graph.RotationSystem.componentDualFaceVertexEquiv {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : ↥(r.dualRotation.componentFaceIndices (r.dualDartEquiv d).vertex) ≃ ↥(G.componentVertexSet d.vertex)

In each edge component, every dual face is exactly one nonempty source vertex fiber. Declared isolated source points are absent from this dart-indexed correspondence.

theorem Cslib.Complexity.Graph.RotationSystem.card_component_dual_faces_eq_vertices {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : (r.dualRotation.componentFaceIndices (r.dualDartEquiv d).vertex).card = (G.componentVertexSet d.vertex).card

The dual face count in an edge component is its number of distinct source vertices.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_iff_component_cards {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) : r.NumericalGenusZero ↔ ∀ (d : G.Dart), (G.componentVertexSet d.vertex).card + (r.componentFaceIndices d.vertex).card = (G.componentEdgeSet d.vertex).card + 2

The existing componentwise numerical predicate is exactly Euler on these finite sets. Point components retain their original conventional face and impose no dart-index condition.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_dual_iff {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) : r.dualRotation.NumericalGenusZero ↔ r.NumericalGenusZero

Actual indexed dualization preserves the existing componentwise numerical genus-zero predicate. Source point components are dropped, and their conventional Euler equations are tautologies on the source side. The empty graph is included. No geometric premise is used.