Two-edge connectivity of one-vertex-cut factors

Complement symmetry of cutMultiplicity, inheritance of the two-edge cut condition by both factors of a OneVertexCut, and the two-vertex lower bound for positive genus. Rehomed from OnceMarkedVertexCutOneFour.lean (which imports this file) so that the bridgeless genus-two classification does not depend on the once-marked census.

Complement symmetry of cut multiplicity

theorem Utilities.cutMultiplicity_compl (H : CFGraph) (S : Finset H.V) : cutMultiplicity H S = cutMultiplicity H Sᶜ

Cut multiplicity counts the edges between a vertex set and its complement, so it is unchanged by complementation.

Two-edge connectivity passes to the factors of a one-vertex cut

theorem Utilities.OneVertexCut.twoEdgeCutCondition_leftGraph {K : CFGraph} (cut : OneVertexCut K) (hTwoEdge : TwoEdgeCutCondition K) : TwoEdgeCutCondition cut.leftGraph

Two-edge connectivity is inherited by the left factor of a one-vertex cut. No genus, degree, or connectivity hypothesis is needed beyond the condition on the ambient graph.

theorem Utilities.OneVertexCut.twoEdgeCutCondition_rightGraph {K : CFGraph} (cut : OneVertexCut K) (hTwoEdge : TwoEdgeCutCondition K) : TwoEdgeCutCondition cut.rightGraph

Two-edge connectivity is inherited by the right factor as well.

Rigidity of a genus-one factor

theorem Utilities.exists_vertex_ne_of_genus_pos {H : CFGraph} (y : H.V) (hGenus : 0 < H.genus) : ∃ (p : H.V), p ≠ y

A graph of positive genus has at least two vertices: a single vertex carries no edge, since chip-firing graphs are loopless.