Degree shapes of bridgeless genus-two cores

The topological-vertex bound reduces a bridgeless genus-two graph to one of two numerical possibilities. This file records the corresponding exact valence shapes. It is deliberately independent of any bivalent-suppression construction: those shapes are invariants of the original graph as well.

theorem Bananas.exists_degree_four_vertex_of_unique_topological_of_bridgeless_genus_two (G : CFGraph) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) (hCard : (Utilities.topologicalVertices G).card = 1) : ∃ (w : G.V), vertexDegree G w = 4 ∧ ∀ (v : G.V), v ≠ w → vertexDegree G v = 2

If a nontrivial bridgeless genus-two graph has one topological vertex, that vertex has valence four and every other vertex is bivalent.

theorem Bananas.exists_two_trivalent_vertices_of_two_topological_of_bridgeless_genus_two (G : CFGraph) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) (hCard : (Utilities.topologicalVertices G).card = 2) : ∃ (w₁ : G.V) (w₂ : G.V), w₁ ≠ w₂ ∧ vertexDegree G w₁ = 3 ∧ vertexDegree G w₂ = 3 ∧ ∀ (v : G.V), v ≠ w₁ → v ≠ w₂ → vertexDegree G v = 2

If a nontrivial bridgeless genus-two graph has two topological vertices, they are both trivalent and every remaining vertex is bivalent.