Ears

The ear decomposition: lem:subdivision-ear-preserve in both halves, and the step of lem:relative-ear that grows a 2-connected subgraph towards the graph containing it.

Rerouting is the engine of half (a)

Graph.Reaches.reroute says the obvious thing in the one form every consumer wants: if every edge but e survives from G into H, and whatever e joins in G is joined in H by other means, then H reaches whatever G reaches. A walk that took e takes the replacement route instead, and the induction is over the walk.

Its hends premise is stated as "whatever e joins in G is joined in H", not as "the two named ends are joined". That is what makes the premise dischargeable in the case where e is not an edge of G at all: it is then vacuous. Graph.Reaches.across_edge_replacement is the specialisation the subdivision runs on, and it is where the vacuous case is used — its routed premise carries the three-way choice the blueprint's proof makes in prose:

• reroute along the new path — the deleted vertex is not on it, so the path survives whole;
• reroute around the old graph — the deleted vertex is on the path, so the old graph is untouched and the replaced edge was not a bridge (Graph.IsTwoConnected.no_bridge);
• do not reroute at all — the deleted vertex is an end of the replaced edge, so no surviving walk could have taken that edge.

Half (a) is stated for a path

Graph.IsTwoConnected.replace_edge_by_path replaces an edge by a whole path, not by a single new vertex. Nothing in the argument cares how long the replacement is, and the general form is what a subdivision needs: subdividing one edge by one vertex is the case where the path has two edges.

Half (b) does not need the blueprint's freshness hypothesis

Graph.IsTwoConnected.ear attaches an ear, and the blueprint's "whose internal vertices are new" is not assumed — the proof does not use it. What carries the argument is Graph.IsPathGraph.reaches_an_end: whatever vertex is deleted, every remaining vertex of the path still reaches one of the two ends. The two ends live in a 2-connected graph, at least one of them survives the deletion, and that survivor is the hub everything routes through.

Half (a) does use freshness, and for a real reason: without it the deleted vertex could sit both on the replacement path and inside the old graph, and then neither of the two routes between the replaced edge's ends need exist.

Finding the ear

Graph.IsTwoConnected.ear_exists needs neither the components of G - V(H) nor a shortest path, which is what the blueprint's proof reaches for. The ear is found: walk out of the subgraph to a vertex outside it, take the edge where the walk first leaves the subgraph (Graph.IsWalk.crossing), and walk back from that edge's outer end to a different vertex of the subgraph inside G minus the edge's inner end — a graph that is connected because G is 2-connected, and whose walks therefore never touch the inner end. That walk with the crossing edge in front is a path of G between two vertices of the subgraph, and the crossing edge is one the subgraph did not have.

Graph.pathGraphOf turns it into a graph and Graph.IsTwoConnected.grows_by_ear glues it on. Termination — the blueprint's "finiteness terminates the process" — is not here; this is the single step, and a consumer that counts edges iterates it.

Looplessness

Graph.IsTwoConnected.ear_exists is the one statement here that has to assume the graph has no loop, and the hypothesis is not bureaucracy: adding a loop to a 2-connected graph leaves it 2-connected, so a 2-connected subgraph missing only a loop grows by no ear at all, and the conclusion — a path between distinct vertices — is false. It is used only in the degenerate branch where every vertex is already present and the missing object is an edge. A plane consumer discharges it from its drawing.

Blueprint

• Graph.IsTwoConnected.replace_edge_by_path — lem:subdivision-ear-preserve (a), "every subdivision of G is 2-connected", stated for a replacement path of any length.
• Graph.IsTwoConnected.ear — lem:subdivision-ear-preserve (b), "if P is a path whose distinct endpoints lie in G … then G ∪ P is 2-connected".
• Graph.IsTwoConnected.ear_exists, Graph.IsTwoConnected.grows_by_ear — the step of lem:relative-ear, "G is obtained from H by repeatedly adding paths whose distinct endpoints are already present".
• Graph.Reaches.reroute, Graph.Reaches.across_edge_replacement — the blueprint's "the remaining part of the subdivided edge attaches w to u or v" together with "a 2-connected graph has no bridge", turned into one transfer lemma.

The union of two subgraphs

Graph.union and the two inclusions into it live in Schoenflies/Graph/TwoConnected.lean; this is the inclusion out of it, which the ear construction needs in order to know that the enlarged subgraph is still a subgraph. It is general and belongs beside the other two — the integrator should hoist it.

Rerouting one edge

theorem Graph.Reaches.reroute {α : Type u_1} {β : Type u_2} {G H : Graph α β} {s t : α} {e : β} (hV : G.vertexSet ⊆ H.vertexSet) (hE : ∀ ⦃g : β⦄ ⦃p q : α⦄, G.IsLink g p q → g ≠ e → H.IsLink g p q) (hends : ∀ ⦃p q : α⦄, G.IsLink e p q → H.Reaches p q) (h : G.Reaches s t) : H.Reaches s t

One edge swapped for any route between its ends. If every edge of G other than e links the same pair in H, and whatever e links in G is joined in H by some other means, then H reaches whatever G reaches: a walk that took e takes the replacement route instead.

The premise about e is universally quantified over its ends rather than stated for a named pair, so that it is vacuous when e is not an edge of G — which is the case a vertex deletion produces, and the reason this is the shape that gets used.

theorem Graph.Reaches.across_edge_replacement {α : Type u_1} {β : Type u_2} {G H : Graph α β} {c s t u v : α} {e : β} (hV : (G.deleteVerts {c}).vertexSet ⊆ H.vertexSet) (hl : G.IsLink e u v) (hE : ∀ ⦃g : β⦄ ⦃p q : α⦄, (G.deleteVerts {c}).IsLink g p q → g ≠ e → H.IsLink g p q) (routed : H.Reaches u v ∨ G.Inc e c) (h : (G.deleteVerts {c}).Reaches s t) : H.Reaches s t

The form a subdivision needs. A walk of G - c transfers to any graph holding the surviving edges, provided the replaced edge's ends are joined there or that edge was incident to the deleted vertex — in which case no walk of G - c could have taken it, and the hends premise of Graph.Reaches.reroute is vacuous.

That disjunction is the blueprint's three-way case analysis: route along the replacement, route around the old graph, or do not route at all.

Attaching an ear

theorem Graph.IsTwoConnected.ear {α : Type u_1} {β : Type u_2} {G P : Graph α β} {u v : α} {W : List β} (hG : G.IsTwoConnected) (hcompat : G.Compatible P) (hP : P.IsPathGraph u W v) (huv : u ≠ v) (hu : u ∈ G.vertexSet) (hv : v ∈ G.vertexSet) : (G.union P).IsTwoConnected

lem:subdivision-ear-preserve (b): attaching an ear preserves 2-connectivity. P is a path whose two distinct ends lie in the 2-connected graph G; then G ∪ P is 2-connected.

The blueprint's hypothesis that the ear's internal vertices are new is not needed. Delete a vertex c. One of the ear's two ends survives, and it is the hub: G - c is connected and contains it, and every surviving vertex of the ear reaches one of the two ends inside the ear (Graph.IsPathGraph.reaches_an_end) — an end which, having been reached after the deletion, is itself not c, so it lies in G - c too.

Replacing an edge by a path

theorem Graph.IsTwoConnected.replace_edge_by_path {α : Type u_1} {β : Type u_2} {G P : Graph α β} {u v : α} {e : β} {W : List β} (hG : G.IsTwoConnected) (hl : G.IsLink e u v) (huv : u ≠ v) (hcompat : (G.deleteEdges {e}).Compatible P) (hP : P.IsPathGraph u W v) (hnew : ∀ x ∈ P.vertexSet, x ≠ u → x ≠ v → x ∉ G.vertexSet) : ((G.deleteEdges {e}).union P).IsTwoConnected

lem:subdivision-ear-preserve (a): a subdivision of a 2-connected graph is 2-connected. Stated for a replacement path rather than for a single new vertex, because nothing in the argument cares how long the replacement is; subdividing one edge by one vertex is the case where P has two edges.

Delete a vertex c. One end of the replaced edge survives and is the hub. Everything on the old side reaches it by Graph.Reaches.across_edge_replacement, whose routed premise is discharged by the three-way case analysis: if c is an end of the replaced edge there is nothing to route; if c is an old vertex then it is not on the path — this is where the freshness hypothesis hnew is used — and the path itself joins the ends; and if c is new then the old graph is untouched and has no bridge. Everything on the path side reaches an end of the path, and an end reached after the deletion survived it.

Finding an ear

theorem Graph.IsTwoConnected.ear_exists {α : Type u_1} {β : Type u_2} {G K : Graph α β} (hG : G.IsTwoConnected) (hK : K.IsTwoConnected) (hKG : K ≤ G) (hnl : ∀ ⦃g : β⦄ ⦃x : α⦄, ¬G.IsLoopAt g x) (hproper : (∃ x ∈ G.vertexSet, x ∉ K.vertexSet) ∨ ∃ g ∈ G.edgeSet, g ∉ K.edgeSet) : ∃ (a : α) (b : α) (D : List β) (g : β), G.IsPath a D b ∧ a ≠ b ∧ a ∈ K.vertexSet ∧ b ∈ K.vertexSet ∧ g ∈ D ∧ g ∉ K.edgeSet

A 2-connected subgraph that is not all of a 2-connected graph has an ear. The ear is found, not chosen: if the subgraph already has every vertex then a missing edge joins two of them and is an ear by itself; otherwise a walk out of the subgraph crosses its boundary, and deleting the crossing edge's inner end leaves G connected, so the outer end walks back to a different vertex of the subgraph without passing through the first.

The looplessness hypothesis is used only in the first, degenerate branch, and it cannot be dropped: a 2-connected graph plus a loop is 2-connected, and no ear is missing from it.

theorem Graph.IsTwoConnected.grows_by_ear {α : Type u_1} {β : Type u_2} {G K : Graph α β} (hG : G.IsTwoConnected) (hK : K.IsTwoConnected) (hKG : K ≤ G) (hnl : ∀ ⦃g : β⦄ ⦃x : α⦄, ¬G.IsLoopAt g x) (hproper : (∃ x ∈ G.vertexSet, x ∉ K.vertexSet) ∨ ∃ g ∈ G.edgeSet, g ∉ K.edgeSet) : ∃ (B : Graph α β), B.IsTwoConnected ∧ K ≤ B ∧ B ≤ G ∧ ∃ g ∈ B.edgeSet, g ∉ K.edgeSet

H5: a 2-connected subgraph of a 2-connected graph grows to it by adding ears. One step: the subgraph gains an ear and at least one edge, and is still a 2-connected subgraph of the big graph. Iterating on the number of missing edges is the caller's business — the blueprint's "finiteness terminates the process".