Bridgeless genus-one topology

The intrinsic genus-one factors in the genus-two wedge normal form are two-regular. This is the numerical cycle property needed by an explicit cycle-presentation construction.

theorem Bananas.vertex_degree_eq_two_of_bridgeless_genus_one (G : CFGraph) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 1) (vertex : G.V) : vertexDegree G vertex = 2

Every vertex of a nontrivial bridgeless genus-one graph is bivalent.