, second inequality: \(\kappa ' \le \delta \).

If \(G\) is trivial then \(\kappa ' = 0 \le \delta \). Otherwise take \(v\) with \(d(v) = \delta \); the \(\delta \) edges incident with \(v\) form an edge cut, since deleting them isolates \(v\). Hence \(\kappa ' \le d(v) = \delta \).

A vertex cut is by definition a proper subset of \(V\), so it omits some vertex and therefore has at most \(\nu - 1\) elements; and in the no-vertex-cut case \(\kappa \) is defined to be \(\nu - 1\). Either way \(\kappa \le \nu - 1\).

A minimum vertex cut cannot have size \(0\) — that would make \(G\) disconnected, contradicting hconn — nor size \(1\), since that would exhibit a cut vertex, contradicting hnocut. And if no vertex cut exists at all then \(\kappa = \nu - 1 \ge 3 - 1 = 2\).

The book’s one-liner has to be unwound through Nat.sInf_eq_zero, which splits \(\kappa ' = 0\) into two cases rather than one: \(0\) is attained — \(\emptyset \) is an edge cut, i.e. \(G\) is disconnected outright; or the set being minimised is empty* — no edge cut exists at all, which forces \(V\) to be a subsingleton, since otherwise deleting every edge leaves \(\bot \), and \(\bot \) on a nontrivial \(V\) is disconnected.

These are exactly the book’s "disconnected" and "trivial". Disconnected gives \(\emptyset \) as a vertex cut, so \(\kappa = 0\); subsingleton gives \(\kappa = \nu - 1 = 0\).

Indices are shifted by one to stay in \(\mathbb {N}\): the book’s \(\kappa '(G) = k\) with \(\kappa '(H) = k - 1\) is stated here as \(\kappa '(G) = k + 1\) with \(\kappa '(G - e) = k\), which avoids truncated subtraction entirely.

Take \(F\) realising \(\kappa '(G) = k + 1\); it is nonempty, so pick \(e \in F\). Then \(F \ {e}\) is an edge cut of \(G - e\) of size \(k\), giving \(\kappa '(G - e) \le k\); and \(\kappa '(G - e) \ge k\), because a smaller cut of \(G - e\) together with \(e\) would be a cut of \(G\) of size \(\lt k + 1\), contradicting minimality.

This is the heart of the induction, isolated as a standalone inequality \(\kappa (G) \le \kappa (G - e) + 1\) so that vertexConnectivity_le_edgeConnectivity becomes a three-line calc. Writing \(H = G - e\), the book’s case analysis is: \(H\) has a complete spanning subgraph \(\Rightarrow \) so does \(G\), and \(\kappa (G) = \kappa (H)\); otherwise take \(S\) a vertex cut of \(H\) with \(|S| = \kappa (H)\), and split: \(G - S\) already disconnected \(\Rightarrow \) \(S\) is a vertex cut of \(G\), so \(\kappa (G) \le |S|\); \(G - S\) connected \(\Rightarrow \) \(e\) is a cut edge (bridge) of \(G - S\), and then \(\nu (G - S) = 2\) \(\Rightarrow \) \(\kappa (G) \le \nu (G) - 1 = |S| + 1\), by vertexConnectivity_le_card_pred; \(\nu (G - S) \ge 3\) \(\Rightarrow \) by Exercise 2.3.1(a) \(G - S\) has a cut vertex \(w\), and \(S \cup {w}\) is a vertex cut of \(G\), so \(\kappa (G) \le |S| + 1\).

Every branch lands at \(\kappa (G) \le \kappa (H) + 1\), which is the statement.

, used by vertexConnectivity_le_deleteEdge_succ.

Only part (a) is needed. Since \(G\) is connected, \(\omega (G) = 1\), so the conclusion \(\omega (G - v) \gt \omega (G)\) is "\(G - v\) is disconnected" — i.e. \(\exists \) w, G.IsVertexCut {w}.

The book leaves this as an exercise, so there is no book proof to quote; the argument below is the standard one.

, first inequality: \(\kappa \le \kappa '\).

Induction on \(\kappa '\). Base \(\kappa ' = 0\): \(G\) is trivial or disconnected, so \(\kappa = 0\). Step: given \(\kappa '(G) = k + 1\), pick \(e\) in a minimum edge cut; then \(\kappa '(G - e) = k\), so \(\kappa (G - e) \le k\) by the induction hypothesis, and \(\kappa (G) \le \kappa (G - e) + 1 \le k + 1 = \kappa '(G)\).

The entire four-way case analysis of the book’s second paragraph has been factored out into vertexConnectivity_le_deleteEdge_succ, so what remains here is exactly the induction skeleton.

(Whitney). The full chain \(\kappa \le \kappa ' \le \delta \).

The conjunction of the two halves proved just above, packaged as the book states it. See vertexConnectivity_le_edgeConnectivity for the \(\kappa \le \kappa '\) proof and edgeConnectivity_le_minDegree for \(\kappa ' \le \delta \).

Transfer of a walk into an induced subgraph: a walk all of whose vertices lie in \(s\) witnesses reachability inside G.induce s.

, strengthened to carry the edge-disjointness that Corollary 3.2.1 needs.

InternallyDisjoint p q as defined in this file does not forbid \(p = q\): for adjacent \(u, v\) the single edge satisfies it with \(p = q\), since its only vertices are the two endpoints. So Theorem 3.2 as stated cannot yield a cycle, and the book’s one-line derivation of Corollary 3.2.1 does not go through. Adding p.edges.Disjoint q.edges to the conclusion repairs this; the book gets it for free because its \(d(u,v) = 1\) case produces a genuine cycle via theorem 2.3, not merely two paths.

(Whitney, 1932).

(\(\Rightarrow \)) is discharged by forgetting the extra edge-disjointness conjunct supplied by the strengthened form.

(\(\Leftarrow \)) unpacks the book’s "clearly". Two steps: \(G\) is connected — the hypothesis hands back a path between any two distinct vertices, and Reachable.refl covers \(a = b\); \(G\) has no cut vertex — if \(w\) were one, \(G - w\) would be disconnected, giving \(a, b\) unreachable in \(G - w\). Both supplied paths \(p, q\) must then pass through \(w\) (else reachable_induce_of_support_subset would transport them into \(G - w\)). So \(w\) is a common internal vertex of \(p\) and \(q\), and InternallyDisjoint forces \(w = a\) or \(w = b\) — contradicting that \(a, b\) live in \({w}^{c}\). Then two_le_vertexConnectivity_of_no_cutVertex converts "no cut vertex" into \(\kappa \ge 2\), which is where \(\nu \ge 3\) is consumed.

Travel out along one path and back along the other; because the two paths meet only at the endpoints, the round trip repeats no vertex, so it is a cycle.

! The book’s "immediately" does not transfer directly. As noted on InternallyDisjoint, this file’s predicate permits \(p = q\), so two_connected_iff_two_internally_disjoint_paths alone would let both paths be the same single edge and p.append q.reverse would not be a cycle. The proof must therefore go through the strengthened exists_two_internally_disjoint_paths_of_two_connected, whose extra p.edges.Disjoint q.edges rules that degenerate case out.

The standard device of turning an edge into a vertex, upgrading "any two vertices lie on a common cycle" to "any two edges do".

A block is connected and has no cut vertex, so no single vertex forms a vertex cut; with at least three vertices this means the smallest vertex cut has size at least \(2\), i.e. \(\kappa (G) \ge 2\).

\(\nu \ge 3\) is needed to exclude the degenerate blocks \(K_{1}\) and \(K_{2}\), which have no cut vertex either but whose connectivity is \(0\) and \(1\) respectively.

This is the bridge that lets Corollary 3.2.2 draw on Theorem 3.2.

(Harary, 1962).

The book proves only the even case; the odd case is exercise 3.3.1, so a full Lean proof of the statement as given must supply it.

Note the two "clearly"/"without loss of generality" steps carry real weight in Lean: the WLOG needs \(|V' \cap S| + |V' \cap T| \le |V'| + 2 \lt 2r + 2\), and the "sequence of distinct vertices ... difference at most \(r\)" is a greedy construction requiring an explicit induction on the arc.

The book’s \({x}\) is the ceiling \(\lceil x\rceil \), so \({mn/2}\) is written as the natural-number division \((m * n + 1) / 2\).

Only \(\varepsilon (H_{m,n}) = \lceil mn/2\rceil \) is formalised. The optimality conclusions \(f(m,n) = \lceil mn/2\rceil \) and \(g(m,n) = \lceil mn/2\rceil \) are not stated in this file, since \(f\) and \(g\) (least edge counts over all \(m\)-connected graphs) are not defined here.

a \(k\)-edge-connected graph satisfies \(k\nu \le 2\varepsilon \).

Stated multiplicatively as \(k\nu \le 2\varepsilon \) to stay in the natural numbers and avoid division.

By Theorem 3.1, \(k \le \kappa ' \le \delta \), so every vertex has degree at least \(k\). Summing over all \(\nu \) vertices gives \(\sum _v d(v) \ge k\nu \), and handshaking (Theorem 1.1) says that sum equals \(2\varepsilon \). Hence \(2\varepsilon \ge k\nu \).

A network that survives any \(k\) link failures must give every station at least \(k\) links, so it cannot be sparse — this is exactly the lower bound \(f(m, n) \ge \lceil mn/2\rceil \) of (3.1), which §3.3 shows the Harary graphs attain.

a simple graph with \(\delta \ge \nu - 2\) has \(\kappa = \delta \).

The hypothesis says every vertex is non-adjacent to at most one other vertex, so the graph is complete or very nearly so. Theorem 3.1 already gives \(\kappa \le \delta \), so only \(\kappa \ge \delta \) needs proving: any set of fewer than \(\delta \) vertices fails to disconnect such a dense graph, because any two surviving vertices are either adjacent outright or share a common surviving neighbour.

Part (b) shows the bound is tight — one step less density (\(\delta = \nu - 3\)) already allows \(\kappa \lt \delta \).

a simple 3-regular graph has \(\kappa = \kappa '\).

Theorem 3.1 gives \(\kappa \le \kappa ' \le \delta = 3\), so both parameters lie in \({0, 1, 2, 3}\) and only \(\kappa ' \le \kappa \) needs argument. Given a minimum vertex cut \(S\) of size \(\kappa \), one converts it into an edge cut of the same size by choosing, for each \(v \in S\), a single suitable incident edge — possible precisely because every vertex of a cubic graph has just three neighbours, so the local structure around a cut vertex is tightly constrained.

Cubic graphs are the smallest interesting regular case, and this exercise records that for them the vertex and edge measures of reliability agree — unlike the general situation, where figure 3.2 has \(\kappa = 2 \lt \kappa ' = 3\).

2-edge-connected \(\iff \) two edge-disjoint paths between any two vertices.

The edge analogue of Whitney’s Theorem 3.2, with "internally disjoint" weakened to "edge-disjoint" and vertex cuts replaced by edge cuts.

Edge-disjoint is genuinely weaker than internally disjoint: the two routes may pass through common intermediate stations, as long as they never use the same link.