Structural genus-two preliminaries

The graph-theoretic opening of Theorem 4.13 starts by suppressing no leaves: the no-bridge condition already forces every vertex of a nontrivial graph to have valence at least two. This module records that reduction and its sharp genus-two topological-vertex bound.

theorem Bananas.hasMinimumValenceTwo_of_twoEdgeCutCondition (G : CFGraph) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) : Utilities.HasMinimumValenceTwo G

A nontrivial graph satisfying the no-bridge cut condition has minimum valence two.

theorem Bananas.card_topologicalVertices_le_two_of_bridgeless_genus_two (G : CFGraph) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) : (Utilities.topologicalVertices G).card ≤ 2

A nontrivial bridgeless genus-two graph has at most two vertices of valence at least three. Equality is the theta-core numerology; the strict case is the vertex-wedge-of-cycles branch of Theorem 4.13.

theorem Bananas.topologicalVertices_nonempty_of_bridgeless_genus_two (G : CFGraph) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) : (Utilities.topologicalVertices G).Nonempty

Genus two forces at least one topological vertex once every vertex has valence at least two.

theorem Bananas.card_topologicalVertices_eq_one_or_two_of_bridgeless_genus_two (G : CFGraph) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) : (Utilities.topologicalVertices G).card = 1 ∨ (Utilities.topologicalVertices G).card = 2

Before suppressing bivalent paths, a nontrivial bridgeless genus-two graph has either one or two topological vertices.