Euler counts for a connected indexed rotation

For a graph with an actual dart and a single declared-vertex component, the existing componentwise numerical predicate reduces to one equation using the full face quotient. Singleton face orbits are included. The dart hypothesis explicitly excludes point components; their conventional face is already handled by NumericalGenusZero itself.

noncomputable def Cslib.Complexity.Graph.RotationSystem.connectedFaceEquiv {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hc : ∀ u ∈ G.vertices, ∀ v ∈ G.vertices, RotationCertificate.SameComponent G u v) (d : G.Dart) : r.ComponentFace d.vertex ≃ r.Face

Connectedness identifies every component face with a face of the whole rotation.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_iff_connected_euler {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hc : ∀ u ∈ G.vertices, ∀ v ∈ G.vertices, RotationCertificate.SameComponent G u v) (d : G.Dart) : r.NumericalGenusZero ↔ G.vertices.toFinset.card + Nat.card r.Face = G.edges.length + 2

On a connected graph with an actual edge, numerical genus zero is precisely Euler's single equation. No geometric meaning or recognition algorithm is asserted.