151 Trees
151.1 Trees
Split the vertices into two nonempty groups and collect the edges running between them; deleting them severs every route from one group to the other.
B&M define an edge cut by its shape \([S, \bar{S}]\); this takes the operational characterisation — a subset of edgeSet whose removal leaves \(G\) disconnected — which for connected \(G\) describes the same collections. ! For disconnected \(G\) they diverge, and \(\emptyset \) satisfies this predicate; that is the source of the IsBond defect below.
An edge cut with nothing to spare — remove all of it and the graph falls apart, but put any single edge back and it is connected again. Exercise 2.2.8 characterises when \([S, \bar{S}]\) is a bond: exactly when both \(G[S]\) and \(G[\bar{S}]\) are connected. Bonds are the notion dual to cycles, a duality chapter 12 develops in full — theorem 2.6 here is the mirror of theorem 2.5.
! Defect: \(\emptyset \) is a bond when \(G\) is disconnected. The docstring above claims nonemptiness is automatic because "deleting \(\emptyset \) leaves \(G\) connected" — but that holds only for connected \(G\). For disconnected \(G\), IsEdgeCutSet \(\emptyset \) unfolds to \(\lnot \) G.Connected, which is true, and there is no \(B' \subset \emptyset \) to test, so the minimality clause is vacuous. Hence IsBond G \(\emptyset \), contradicting minimal nonempty edge cut.
The repair: add B.Nonempty as a conjunct, or carry G.Connected as a hypothesis wherever IsBond is used (theorem 2.6 already does — its hG is available).
! \(\tau (G)\) counts the distinct spanning trees, not the non-isomorphic ones. B&M stress the difference: \(K_{6}\) has six non-isomorphic spanning trees (figure 2.1) but \(6^{4} = 1296\) distinct ones. \(\tau \) satisfies deletion–contraction (theorem 2.8) and, for complete graphs, Cayley’s formula (theorem 2.9); the general determinant formula is chapter 12’s matrix-tree theorem.
"Spanning" is automatic: a T : SimpleGraph W lives on the whole vertex type, so T \(\le \) H \(\land \) T.IsTree already means a spanning tree. ! IsTree bundles Connected, which requires Nonempty W — so on an empty carrier \(\tau = 0\). That is where cayley fails at \(n = 0\).
\(G \cdot e\) (§2.4). Mathlib has no edge contraction for SimpleGraph. NOTE: a genuine contraction identifies the ends of \(e\) and therefore changes the carrier type (to \(|V| - 1\) vertices). Here it is stubbed on the same carrier \(V\) as a placeholder, purely so that the deletion–contraction recurrence (Theorem 2.8) can be typed.
Think of \(e = uv\) as a string pulled tight until \(u\) and \(v\) merge; everything attached to either is now attached to the merged vertex, and \(e\) disappears. For a link, \(\nu (G\cdot e) = \nu - 1\), \(\varepsilon (G\cdot e) = \varepsilon - 1\), \(\omega (G\cdot e) = \omega \) — so contracting an edge of a tree again yields a tree, which is what makes deletion–contraction work.
! Defective on two counts. 1. sorry body. \(G \cdot e\) is an opaque graph, so theorem 2.8 relates opaque quantities and asserts nothing. 2. Wrong carrier. A genuine contraction has \(\nu - 1\) vertices; this is stubbed on the same carrier \(V\) purely so theorem 2.8 can be typed. Even given an honest body on \(V\), the identity \(\nu (G\cdot e) = \nu - 1\) could not hold.
The repair is to move to the quotient carrier \({x : V // x \ne v}\) with \(v\)’s incidences re-pointed at \(u\), exactly as chapter 10’s Digraph.contractEdge does — that definition is honest and complete, and can be transcribed.
A tree has exactly enough edges to hold the vertices together and not one more: connectivity gives at least one route between any two vertices, acyclicity forbids a second, since two distinct routes always enclose a cycle. ! The converse holds for loopless graphs (exercise 2.1.1), so "unique paths between all pairs" is an equivalent definition of a tree — that direction is not stated here.
\(\nu - 1\) edges is exactly the price of connecting \(\nu \) vertices acyclically — corollary 2.4.2 shows it is also the minimum price of connecting them at all.
Stated additively as \(\varepsilon + 1 = \nu \) to avoid truncated \(\mathbb {N}\)-subtraction.
A degree-one vertex of a tree is a leaf. ! B&M offer a more illuminating alternative (exercise 2.1.2): take a longest path; both endpoints have degree one, since an extra neighbour would either extend the path or close a cycle. That route would be shorter in Lean too, if exists_path_length_of_minDegree-style machinery from chapter 1 were available.
Cut edges are exactly the edges lying on no cycle: an edge on a cycle has a detour around it, while an edge on no cycle is the sole link between the two sides it joins.
Mathlib’s IsBridge is B&M’s cut edge. Note the conclusion carries G.Adj v w as a conjunct, which IsBridge includes — a non-edge is not a bridge.
A tree is exactly a connected graph with no redundancy — every single edge indispensable for keeping it in one piece. ! Exercise 2.2.1, not stated here, drops the connectivity hypothesis: \(G\) is a forest iff every edge is a cut edge.
Keep deleting redundant edges — those lying on cycles — until none remain; what is left still connects everything but has no cycle. * This is the workhorse of the rest of the chapter: corollary 2.4.2, theorem 2.6 and corollary 2.7 all open by invoking it.
\(\nu - 1\) edges is the minimum price of connecting \(\nu \) vertices, and trees are precisely the connected graphs paying exactly that price. ! Compare exercise 2.1.5, not stated here: for a graph with exactly \(\nu - 1\) edges, connected, acyclic and tree are all equivalent.
A spanning tree already offers a unique route between the ends of \(e\); adding \(e\) supplies a second, and the two close off precisely one cycle — the fundamental cycle of \(e\) with respect to \(T\). * The engine of the exchange argument for Kruskal’s optimality (theorem 2.10), and of chapter 12’s tree-basis of the cycle space.
! Only the existence half is stated: uniqueness of a cycle in Lean holds only up to rotation and reflection of the walk, which is awkward to phrase directly. Chapter 12’s fundamentalCycle needs the uniqueness half, so this gap propagates there.
The exact mirror of theorem 2.5, with cycle \(\to \) bond and *spanning tree \(\to \) cotree*. * Chapter 12’s fundamentalBondVertexSet is exactly the \(S\) of step 3, and cites this theorem by name.
! Both parts consume IsBond, whose \(\emptyset \) defect is active here — but hG : G.Connected is available as a hypothesis, which is precisely the condition under which the defect disappears. Use it explicitly rather than relying on it silently.
In a tree the cut vertices are exactly the internal (non-leaf) vertices.
! Step 2’s exercise 2.1.5 is the one real import; Mathlib’s IsAcyclic API may supply it more directly than reproving the book’s route.
However tangled a connected graph is, there are always at least two vertices you can delete without breaking it apart.
Iterating the recursion reduces any graph to trivial ones and so computes \(\tau \) — though B&M note it is impractical for large graphs, which is what motivates chapter 12’s determinant formula.
! Currently vacuous. contract has a sorry body, so \(G \cdot e\) is opaque and this statement relates opaque quantities. Worse, contract is a same-carrier placeholder, so even an honest body on \(V\) could not satisfy \(\nu (G\cdot e) = \nu - 1\) and step 3’s bijection would be false. Repair contract on the quotient carrier first — see its docstring.
! B&M caution that \(n^{n-2}\) counts distinct spanning trees, not non-isomorphic ones: \(K_{6}\) has six non-isomorphic ones but \(6^{4} = 1296\) distinct.
Mathlib has no Cayley formula and no Prüfer correspondence, so all four steps are from scratch — the largest single item in the chapter.
Assign each edge a weight and each spanning tree the total; the connector problem asks for the least, and theorem 2.10 guarantees Kruskal’s greedy procedure — repeatedly take the cheapest edge not closing a cycle — always finds one.
! The algorithm is a procedure, not a proposition, so what is stated is the mathematical target it attains: existence of a minimum-weight spanning tree. That is strictly weaker than theorem 2.10, which asserts the *greedy output* is optimal — the exchange argument quoted above is not exercised by the skeleton, which is a three-line finiteness argument instead. Formalising the real theorem would need Kruskal’s algorithm defined first. Weights are \(\mathbb {R}\)-valued, matching B&M’s remark that the algorithm is valid for arbitrary real weights.