Cardinalities of component faces and dense vertex names

These facts connect actual face quotients with the existing least-index representative counts. They include singleton face orbits and arbitrary declared root names. Dense vertex counts reuse Cslib.Complexity.Graph.card_componentVertexSet rather than a separate list-count proof.

Main definitions

• Cslib.Complexity.Graph.RotationSystem.ComponentFace: faces in one declared component.

Main results

• Cslib.Complexity.Graph.RotationSystem.count_faceRepresentatives_eq_card_componentFace: the numerical Euler face count equals the cardinality of actual component faces.
• Cslib.Complexity.Graph.countP_vertices_range: component counts for dense vertex names.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationSystem.ComponentFace {G : Graph} (r : G.RotationSystem) (root : ℕ) : Type

Actual face classes with a dart in the declared component of root.

theorem Cslib.Complexity.Graph.RotationSystem.componentFace_mk_iff {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (root : ℕ) (d : G.Dart) : (∃ (e : G.Dart), RotationCertificate.SameComponent G root e.vertex ∧ ⟦e⟧ = ⟦d⟧) ↔ RotationCertificate.SameComponent G root d.vertex

A face represented by a dart belongs precisely to that dart's component.

theorem Cslib.Complexity.Graph.RotationSystem.card_componentFaceRepresentatives {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (root : ℕ) : Nat.card { d : G.Dart // RotationCertificate.SameComponent G root d.vertex ∧ r.IsFaceRepresentative d } = Nat.card (r.ComponentFace root)

Exactly one representative in a component is counted for each actual face.

theorem Cslib.Complexity.Graph.RotationSystem.count_faceRepresentatives_eq_card_componentFace {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (root : ℕ) : 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)) = Nat.card (r.ComponentFace root)

The numerical face count equals the cardinality of the full component face quotient.

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

Old face steps preserve each declared component selection.

theorem Cslib.Complexity.Graph.countP_vertices_range (G : Graph) (n : ℕ) (hG : G.vertices = List.range n) (root : ℕ) : List.countP (fun (v : ℕ) => decide (RotationCertificate.SameComponent G root v)) G.distinctVertices = Nat.card { v : Fin n // RotationCertificate.SameComponent G root ↑v }

Declared dense vertex names can be counted directly as a subtype of Fin n.