Topological vertices

After grafted trees have been pruned, the low-genus classification treats vertices of valence at least three as topological vertices. The minimum-valence-two hypothesis is essential for bounding their number in terms of the genus.

def Utilities.topologicalVertices (G : CFGraph) : Finset G.V

The vertices of valence at least three.

Equations

• Utilities.topologicalVertices G = {v : G.V | 3 ≤ vertexDegree G v}

def Utilities.HasMinimumValenceTwo (G : CFGraph) : Prop

Every vertex has valence at least two. This is the structural condition obtained after pruning grafted trees.

Equations

• Utilities.HasMinimumValenceTwo G = ∀ (v : G.V), 2 ≤ vertexDegree G v

theorem Utilities.vertex_degree_pos_of_connected_of_exists_vertex_ne {G : CFGraph} (hConnected : graphConnected G) (hOther : ∀ (vertex : G.V), ∃ (other : G.V), other ≠ vertex) (vertex : G.V) : 0 < vertexDegree G vertex

Connectivity across a singleton cut gives positive valence whenever the graph has a vertex distinct from each chosen vertex. The genus-specific leafless-normalization arguments supply the second-vertex hypothesis from their edge-count identities; keeping that argument separate makes this singleton-cut step reusable at every genus.

theorem Utilities.hasMinimumValenceTwo_of_leafless_of_exists_vertex_ne {G : CFGraph} (hConnected : graphConnected G) (hOther : ∀ (vertex : G.V), ∃ (other : G.V), other ≠ vertex) (hLeafless : ∀ (vertex : G.V), vertexDegree G vertex ≠ 1) : HasMinimumValenceTwo G

A connected leafless graph with at least two vertices has minimum valence two. This is the common first step before suppressing bivalent chains in a loop-aware normalizer.

def Utilities.IsTopologicallyTrivalent (G : CFGraph) : Prop

Every vertex is bivalent or trivalent.

Equations

• Utilities.IsTopologicallyTrivalent G = ∀ (v : G.V), vertexDegree G v = 2 ∨ vertexDegree G v = 3

theorem Utilities.sum_vertex_degree_sub_two (G : CFGraph) : ∑ v : G.V, (vertexDegree G v - 2) = 2 * G.genus - 2

The sum of the valence excesses over two is 2g - 2.

theorem Utilities.card_topologicalVertices_le (G : CFGraph) (hMin : HasMinimumValenceTwo G) : ↑(topologicalVertices G).card ≤ 2 * G.genus - 2

A graph of minimum valence two has at most 2g - 2 topological vertices.

theorem Utilities.card_topologicalVertices_eq_of_topologicallyTrivalent (G : CFGraph) (hTri : IsTopologicallyTrivalent G) : ↑(topologicalVertices G).card = 2 * G.genus - 2

In a bivalent/trivalent graph, the number of trivalent vertices is exactly 2g - 2.

theorem Utilities.card_topologicalVertices_eq_six_of_genus_four (G : CFGraph) (hTri : IsTopologicallyTrivalent G) (hGenus : G.genus = 4) : (topologicalVertices G).card = 6

A topologically trivalent genus-four graph has six topological vertices.

theorem Utilities.card_topologicalVertices_eq_eight_of_genus_five (G : CFGraph) (hTri : IsTopologicallyTrivalent G) (hGenus : G.genus = 5) : (topologicalVertices G).card = 8

A topologically trivalent genus-five graph has eight topological vertices.