150 Planar Graphs
150.1 Planar Graphs
The walk may start and end on \(H\), but between those endpoints it must stay entirely outside \(H\). This is what makes the bridge relation an equivalence, and it is why a bridge is a maximal chunk of the graph hanging off \(H\) and touching it only at its attachment points.
p.support.tail.dropLast is the walk’s interior — drop the first vertex (tail) and the last (dropLast). ! This is not the repo’s InternallyDisjoint (TwoConnected.lean:58), which relates a walk to another walk; here the second argument is a Subgraph. A walk of length \(\le 1\) has empty interior and so is vacuously internally disjoint from everything — which is intended, and is what makes bridgeRel reflexive on single edges.
Two edges outside \(H\) are related when you can travel from one to the other without passing through \(H\). Grouping edges into classes carves \(G - E(H)\) into the pieces that hang off \(H\) — those pieces are the bridges.
Relation.EqvGen wraps the book’s raw condition in its reflexive–symmetric–transitive closure, which discharges the book’s "it is easy to verify" rather than proving it: whatever the raw relation does, the closure is an equivalence by construction. This is a deliberate trade — the file gains an equivalence for free, at the cost that bridgeRel is a priori coarser than \(\sim \). It is not actually coarser (the book’s \(\sim \) really is an equivalence), but nothing here proves that, so do not appeal to "bridgeRel e f gives a single connecting walk" — it gives a chain of them. Several skeletons below rely on this distinction.
A bridge is one of the connected pieces remaining when \(H\) is removed, together with the attachment points where it touches \(H\). The three "immediate" facts quoted above are bridgeOf_connected, exists_path_internallyDisjoint and bridge_inter_subset_cycle below — none of them is actually immediate once \(\sim \) is a closure. In planar graph theory bridges carry the argument: theorem 9.8 says inner bridges of a cycle avoid one another, theorem 9.9 that a bridge avoiding every outer bridge is transferable, and together these drive Kuratowski’s theorem 9.10.
Indexed by a representative edge \(e\) rather than by a class, so "the bridge containing \(e\)"; two edges give the same bridge exactly when bridgeRel H e f. Built with Subgraph.mk directly — not with SimpleGraph.toSubgraph (Subgraph.lean:559), which is spanning and would put every vertex of \(G\) into every bridge. Note verts is the union of the class’s edges, so it automatically includes the attachment points.
! Because bridgeRel is reflexive for any \(e\) (it is an EqvGen), bridgeOf H e is nonempty even for an \(e\) that is not an edge of \(G\) at all — it then has two vertices and no edges. Statements about bridges must therefore carry e \(\in \) G.edgeSet \{} H.edgeSet explicitly. Two of them below originally omitted it and were false as a result; both now carry it (see the module header).
The points at which the bridge touches down onto the cycle. Almost everything in §9.4 is a statement about how two bridges’ attachment sets interleave around \(C\) — Overlaps, Skew and the segments below are all built on this one set.
Specialised to H = c.toSubgraph for a closed walk \(c\), since §9.4 only ever needs bridges of a cycle. A Set V, not a Finset, so that .ncard is used for \(k\) (see theorem 9.6’s conclusion). "\(B\) is a \(k\)-bridge" is spelled (G.attach c e).ncard = k, and "\(B\) and \(B'\) are equivalent" is G.attach c e = G.attach c e’.
Walking around the cycle from its base point, this records how many steps it takes to reach \(x\). Comparing indices is how "cyclic order" is expressed here.
! Mathlib’s CircularOrder/Btw/SBtw are order classes on a type and do not apply to the support list of a particular cycle, so they are no help. ! List.idxOf silently returns the list’s length for an absent element, so every use must be guarded by x \(\in \) c.support — unguarded, all missing vertices quietly share one position past the end. Note also that this is genuinely linear, not cyclic: it is measured from \(c\)’s base point, so InCyclicOrder below expresses a cyclic condition only up to the choice of that base point.
Travelling once round the cycle, the four vertices are met in that order. This is the configuration making two bridges skew: each bridge’s two attachments separate the other’s, so drawn inside the same region their connecting paths would have to cross — which is precisely the Jordan-curve contradiction in theorem 9.8.
Rendered as a chain of strict cycleIdx inequalities, i.e. as a linear order from \(c\)’s base point rather than a genuinely cyclic one. This is weaker than the book’s phrase: the book’s "cyclic order \(u, u', v, v'\)" is invariant under rotation, whereas this version distinguishes rotations. It suffices for Skew, which existentially quantifies over which attachment plays which role and so recovers rotation-invariance, but do not reuse InCyclicOrder where genuine rotation-invariance is needed.
Stand at \(a\) and walk forwards around the cycle; this counts the steps until \(x\) is reached. Unlike cycleIdx — which is measured from \(c\)’s own base point and so is merely linear — this is genuinely cyclic: it is what lets an arc "wrap round" past the base point.
! Guard uses by a, x \(\in \) c.support. cycleIdx returns c.support.length for an absent vertex, which here yields a meaningless distance. For \(a\) on the cycle the \(\mathbb {N}\)-subtraction never truncates: cycleIdx a \(\le \) c.length (the base point occurs first at index \(0\)), so cycleIdx x + c.length \(\ge \) cycleIdx a. The % c.length is what performs the wraparound; for a degenerate \(c\) of length \(0\) it is the identity (\(n \% 0 = n\) in Lean), which is harmless since every use site carries hc : c.IsCycle.
Walking forwards from \(a\), you meet \(x\) no later than \(b\). Both endpoints count as being on the arc, matching the book’s segments, which share their endpoints with the neighbouring segments and so are edge-disjoint but not vertex-disjoint.
Stated via cycleDist, so the wraparound is handled: the arc from \(a\) to \(b\) may pass through \(c\)’s base point. The x \(\in \) c.support conjunct is the guard that keeps vertices off the cycle out, since cycleDist would otherwise give them a spurious finite distance.
The arc from \(a\) forwards to \(b\) is then exactly one segment of the bridge — an arc of \(C\) with attachments at both ends and none in between. Ranging over all consecutive pairs recovers the book’s partition of \(C\).
"No attachment strictly between" is phrased as: every attachment on the closed arc is one of the two endpoints. This is what makes the segments partition \(C\) rather than merely cover it. The definition does not require the bridge to have \(k \ge 2\) attachments; with fewer, no pair satisfies it, and Avoids below is then false for want of a witness — which is the right answer, since a \(0\)- or \(1\)-bridge has no segments to contain anything.
Cut the cycle at one bridge’s attachment points, producing arcs; the two bridges avoid each other when the second’s attachments all fall inside a single arc, so both can be drawn on the same side of \(C\) without crossing.
The disjunction mirrors the book’s "of one bridge …of the other", which is not symmetric on its face — the definition says only that some assignment of the two roles works. A segment of the bridge of \(e\) is the arc OnArc a b for \(a\), \(b\) consecutive attachments of \(e\).
Neither bridge’s attachments fit inside a single segment of the other, so drawn on the same side of \(C\) they would be forced to cross. Theorem 9.8 says this cannot happen for two inner (or two outer) bridges of a plane graph, and theorem 9.6 says overlapping comes in only two shapes.
! Repaired — previously sorry. This definition formerly had the body Prop := sorry, making it an opaque, unspecified proposition and rendering overlap_imp_skew_or_equivalent_three_bridge (theorem 9.6) vacuous: with Overlaps opaque, that theorem said nothing about bridges and "proving" it would have established nothing. It also violated the project convention (.claude/CLAUDE.md): never sorry in a def — a sorry-ed proof is an honest debt, a sorry-ed definition is a silent change of meaning.
It is now the honest negation of Avoids, built on the segment machinery above (cycleDist \(\to \) OnArc \(\to \) ConsecutiveAttach \(\to \) Avoids), which is the layer B&M assume when they speak of segments. ! [DecidableEq V] had to be added to the signature, since cycleIdx needs it; every use site already had the instance.
The two bridges interleave around the cycle. In a plane graph this is fatal for two bridges on the same side: their connecting paths would have to cross, contradicting the Jordan curve theorem — which is exactly the (dropped) proof of theorem 9.8.
The book asks for four distinct vertices; the Lean version requires only \(a \ne b\) and \(a' \ne b'\). The remaining distinctness is implied by the strict cycleIdx chain in InCyclicOrder, since distinct indices force distinct vertices — provided all four lie on c.support, which the attach memberships supply. Rotation-invariance is recovered by the existential over which attachment plays which role, compensating for InCyclicOrder being measured from \(c\)’s base point.
A cycle no shorter than any other cycle of \(G\). This is the standard extremal device: assume the longest cycle is not a Hamilton cycle, then derive a contradiction from the structure of the bridges hanging off it. That is exactly how Chvátal–Erdős is proved below.
! Not girth/egirth, which are the shortest cycle — the opposite extremum. The maximality clause quantifies over cycles at every base point \(w\), not just at \(u\), which is what makes it a genuine global maximum. Note the definition does not assert existence: IsLongestCycle is a hypothesis to be supplied, and producing one requires knowing \(G\) has a cycle at all.
A planar graph cannot be everywhere dense: Euler’s formula caps its edge count at \(3\nu - 6\), so the average degree is below \(6\) and some vertex has degree at most \(5\). This is the fact driving the five-colour theorem 9.11 — every planar graph has a vertex of degree at most five to induct on — and it is why the arithmetic core was worth salvaging even though the planarity around it was not.
! This is not corollary 9.5.3 as the book states it. Planarity is replaced by the hypothesis \(h\varepsilon \), which corollary 9.5.2 (dropped, being unstatable without faces) would have supplied. Ship it under the name minDegree_le_five_of_card_edge_le, never as planar_minDegree_le_five: the theorem proved is the arithmetic half only. Stated additively (\(\varepsilon + 6 \le 3\nu \)) to dodge truncated \(\mathbb {N}\)-subtraction.
Worth knowing while filling: h\(\nu \) : 3 \(\le \) Fintype.card V is unused. Steps 1–4 never mention \(\nu \) except through the two inequalities \(2\varepsilon + 12 \le 6\nu \) and \(6\nu \le 2\varepsilon \), whose contradiction is independent of the size of \(\nu \). The book needs its \(\nu = 1, 2\) caveat because it invokes corollary 9.5.2, which carries \(\nu \ge 3\); once that corollary is replaced by the raw hypothesis \(h\varepsilon \), the caveat evaporates. \(h\nu \) is kept only so the statement still reads as the book’s; do not go looking for a place to use it.
\(\varepsilon (G) + \varepsilon (G^{c}) = C(\nu , 2)\).
Every unordered pair of distinct vertices carries an edge in exactly one of \(G\) and \(G^{c}\) — that is precisely what complementation means — so the two edge counts partition the \(C(\nu , 2)\) available pairs. Together with the planar edge bound applied to both graphs, this is the whole of exercise 9.3.3(a).
! Missing from Mathlib (0 hits at the time of writing; step 3 is the part most likely to exist already, so search before building). Needs both DecidableRel G.Adj and DecidableRel G\(^{c}\).Adj as instances, since edgeFinset is only available with decidable adjacency.
Planarity forces sparsity, and a graph and its complement cannot both be sparse: between them they must carry every possible edge, and \(C(\nu ,2)\) outgrows \(2(3\nu -6)\) at exactly \(\nu = 11\). Part (b) of the exercise confirms the bound is sharp in spirit — there is a simple planar graph on \(\nu = 8\) vertices whose complement is also planar.
! This is not exercise 9.3.3(a) as stated. "Planar" is replaced by the corollary-9.5.2 edge bound on both sides, so what is proved is that the two bounds are jointly unsatisfiable — the arithmetic obstruction, with the topology stripped out. The conclusion is therefore a negated conjunction rather than "\(G^{c}\) is nonplanar".
Bridges can only meet on \(H\) itself. If a vertex outside \(H\) lay in two bridges, edges of both would meet there, and a walk through it from one to the other stays outside \(H\) — so those edges are related and the two bridges were the same class all along. This is what makes the bridge decomposition genuinely a decomposition: the bridges partition \(E(G) \ E(H)\) and meet only at attachment points.
"Distinct bridges" is hne : \(\lnot \) G.bridgeRel H e e’ — two representative edges in different classes — rather than a disequality of subgraphs, which would be weaker and harder to use. The hypotheses \(he\), \(he'\) placing both edges in G.edgeSet \{} H.edgeSet are present and are needed: without them bridgeOf degenerates (see its docstring).
A bridge is one connected lump: its edges all lie in one \(\sim \)-class, and \(\sim \) relates edges precisely when a walk avoiding \(H\)’s interior joins them.
Together with exists_path_internallyDisjoint this is one of two facts B&M wave through and that everything downstream (theorems 9.6, 9.7 and exercise 9.4.3) actually consumes. Step 3 is the real content and is worth extracting as a lemma about bridgeRel chains, since the same induction is needed for the companion result.
Not only is a bridge connected, but the connection can be made without re-entering \(H\). This is the form actually used downstream: theorem 9.7 needs \((v_{1},v_{2})\)-paths inside a bridge avoiding the cycle internally, and the dropped theorem 9.8 needs the same to reach its Jordan-curve contradiction.
The path is asked for as a G.Walk, not a walk in the bridge. That is equivalent and more convenient: a walk in \(G\) between two bridge vertices that is internally disjoint from \(H\) automatically has all its edges in the bridge’s class. Note the trans case in step 1 is the reason this is genuinely harder than bridgeOf_connected and not a corollary of it.
The picture is a tripod: a hub \(v_{0}\) strictly off the cycle, with three legs reaching down to the three attachment points. This is what the dropped theorem 9.8 uses to dispose of equivalent 3-bridges, and what Kuratowski’s theorem 9.10 uses to locate \(K_{3,3}\) subdivisions.
The "only the vertex \(v_{0}\) in common" conditions are spelled as three \(\forall \) x, x \(\in \) _.support \(\to \) x \(\in \) _.support \(\to \) x = v\(_{0}\) clauses rather than as set equalities, which is what the takeUntil/dropUntil lemmas deliver directly. Note step 5 is genuinely extra work: the book states \(v_{0} \in V(B) \ V(C)\) in the theorem but never justifies it in the proof.
Overlapping comes in exactly two flavours. This dichotomy is what the dropped theorem 9.8 disposes of — the skew case by the Jordan curve theorem, the equivalent-3-bridge case by the tripod of theorem 9.7. It is the reason theorem 9.7 exists at all.
"Equivalent 3-bridges" is rendered as the conjunction attach c e = attach c e’ \(\land \) (attach c e).ncard = 3, matching the book’s definition of equivalent \(k\)-bridges. Steps 2–4 all reduce to arc arithmetic on cycleIdx, so the segment machinery built for Overlaps will carry most of them.
Since \(G\) is not hamiltonian the longest cycle misses some vertex; connectivity joins that vertex to the cycle, and the joining path’s edges lie in a bridge that therefore reaches off \(C\). This is the setup for the whole exercise — that bridge is the object whose attachments part (ii) constrains, and Chvátal–Erdős falls out of those constraints.
Note this is the only one of the three 9.4.3 statements that carries hnh; part (ii) as stated below drops it, which is where its defect comes from.
The successors of a bridge’s attachment points form an *independent set*. That is exactly the leverage Chvátal–Erdős needs: a bridge with many attachments yields a large independent set, which \(\alpha \le \kappa \) forbids.
Indices are into the walk (c.getVert i), so \(i + 1\) is the successor along \(c\); the wraparound at the end of the support is handled by getVert saturating, which is why step 3 must be phrased as two explicit arcs rather than as index arithmetic mod \(n\).
\(\alpha \) is the independence number and \(\kappa \) the connectivity, so the hypothesis says the graph is at least as well connected as it is "spread out". This is one of the most elegant sufficient conditions for hamiltonicity known, and the whole bridge apparatus of §9.4 that survives in this file exists to reach it — it is the prize of the surviving combinatorial core.
! h\(\nu \) : 3 \(\le \) Fintype.card V is load-bearing and is not in B&M — the statement is false without it. \(K_{2}\) has \(\alpha = 1\) and \(\kappa = 1\), so \(\alpha \le \kappa \) holds, yet \(K_{2}\) has no Hamilton cycle, there being no cycle of length two. (\(K_{1}\) is similar.) Step 5 is where most of the work sits; step 4’s cut argument is the part most likely to need its own supporting lemma.
A cubic hamiltonian graph splits into an even cycle plus a perfect matching; two colours alternate around the cycle and the third takes the matching.
Why this matters (§9.7). Tait (1880) showed the four-colour conjecture equivalent to "every simple 3-regular 3-connected planar graph has a Tait colouring" (theorem 9.12(iii)), and then by mistakenly assuming that every such graph is hamiltonian, gave a "proof" of the conjecture using exactly this exercise. Over half a century later Tutte (1946) exhibited a nonhamiltonian 3-regular 3-connected planar graph, invalidating the argument. So this exercise is sound; only Tait’s extra assumption was not.
A Tait colouring is spelled G.lineGraph.Colorable 3, needing no new definitions — lineGraph has the edges of \(G\) as vertices, adjacent when they share an end, so a proper colouring of it is a proper edge colouring of \(G\). Step 3’s parity assignment is the fiddly part: it needs a function from an edge of \(c\) to its index along \(c\), which c.edges provides as a list position.