A cycle, as two paths sharing their ends, is 2-connected

lem:union-two-connected says a union of two 2-connected graphs sharing two vertices is 2-connected. Its companion is the base case: a cycle — two internally disjoint paths with the same two ends — is 2-connected, and neither path is 2-connected on its own, so the union lemma cannot deliver it.

Stated for an ambient graph K that the two paths cover, rather than for Graph.union, so that a geometric consumer never has to prove a graph equality — which is the form in which the consumers actually arrive.

This is the general lemma extracted from a second, independent attempt at Schoenflies.squaresTwoConnected (the one that landed is Schoenflies/SquareCycle.lean, by a different route). It is kept because it is reusable and because at least two consumers want it: the anchored square mesh of prop:anchored-square-mesh, whose collar rectangles are attached one cycle at a time, and any later argument that has to see a subdivided closed curve as a 2-connected graph.

Blueprint

• Graph.isTwoConnected_of_two_paths — the cycle base case of lem:union-two-connected.

theorem Graph.isTwoConnected_of_two_paths {α : Type u_1} {β : Type u_2} {K P Q : Graph α β} {u v : α} {W₁ W₂ : List β} (hPK : P ≤ K) (hQK : Q ≤ K) (hV : K.vertexSet ⊆ P.vertexSet ∪ Q.vertexSet) (hP : P.IsPathGraph u W₁ v) (hQ : Q.IsPathGraph u W₂ v) (huv : u ≠ v) (hmeet : ∀ x ∈ P.vertexSet, x ∈ Q.vertexSet → x = u ∨ x = v) (h3 : K.HasThreeVertices) : K.IsTwoConnected

A graph covered by two paths with the same two ends, meeting only there, is 2-connected.

Stated for an ambient graph K that the two paths cover, rather than for Graph.union, so that a geometric consumer never has to prove a graph equality.

Deleting a vertex c: every surviving vertex reaches an end of its own path (Graph.IsPathGraph.reaches_an_end). If c is neither end, then c misses one of the two paths — they share only u and v — and that whole path still joins u to v, so u is a hub. If c is an end, the branch reaching it is impossible (a deleted vertex is reached by nothing) and the other end is the hub.