Start with a \(k\)-chromatic graph and keep deleting vertices and edges as long as the chromatic number stays at \(k\). The graph is finite, so this stops; what remains is still \(k\)-chromatic but every proper subgraph of it needs fewer colours — that is, it is \(k\)-critical. This is the reduction that makes critical graphs worth studying at all: any statement proved for \(k\)-critical graphs transfers to all \(k\)-chromatic ones. Corollary 8.1.1, Brooks’ theorem 8.4 and theorem 8.5 all open by invoking it.

Only [Finite V] is needed, not [Fintype V]: the argument uses finiteness solely to well-found the minimisation in step 2.

If a graph were disconnected, its chromatic number would be the maximum of those of its components — colour each component independently. So one component already achieves \(\chi (G)\), and that component is a proper subgraph with the same chromatic number, contradicting criticality. Corollary 8.2 strengthens this considerably: every critical graph is not merely connected but a block, having no cut vertex at all.

Step 3 is the whole content and is reusable: the same "components colour independently" lemma is exercise 8.4.6 in its counting form (\(\pi _k\) multiplies over components). Worth proving once in a shared form.

A vertex of small degree is never an obstacle to colouring, since some colour is always free for it. So a graph that genuinely needs \(k\) colours, minimally, cannot contain such a vertex — criticality is what turns "\(v\) is easy to colour" into a contradiction rather than merely an observation.

\(k - 1\) is \(\mathbb {N}\)-subtraction, but the statement is a lower bound, so truncation is harmless: at \(k = 0\) it reads 0 \(\le \) minDegree. Step 4 is where the strict inequality \(\delta \lt k - 1\) is spent, so it needs \(k \ge 1\) to know Fin (k-1) is the right palette — available from \(h.1\) as in step 1.

Needing \(k\) colours is not a global accident — it forces \(k\) distinct vertices each locally rich enough (degree \(\ge k - 1\)) to be part of the obstruction. The critical subgraph is what localises the difficulty; without it, "\(G\) needs \(k\) colours" says nothing about any individual vertex.

Step 3 is stated about G.degree, not H.coe.degree, which is why the filter in the goal mentions only \(G\) — the critical subgraph is existential and does not appear in the statement.

Colour the vertices one at a time in any order: when a vertex’s turn comes it has at most \(\Delta \) neighbours, so at most \(\Delta \) colours are forbidden and one of \(\Delta + 1\) is always free. The book observes the bound *is sometimes very much greater than the actual value* — bipartite graphs are 2-chromatic with arbitrarily large \(\Delta \) — making it weaker than Vizing’s edge analogue (theorem 6.2) in one sense; and weaker in a second sense too, since many graphs satisfy \(\chi ' = \Delta + 1\) whereas Brooks’ theorem 8.4 shows only two families satisfy \(\chi = \Delta + 1\).

The book’s route is recorded because it is the book’s, but the direct route is preferred: it avoids depending on exists_isKCritical_subgraph and IsKCritical.minDegree_ge, both of which are substantially harder than this corollary. This is the cheapest genuine win in the file — a good first fill.

A clique cut is too rigid to cause trouble: its vertices are forced to take distinct colours anyway, and distinct colours can always be permuted into agreement, so the pieces reconcile and the graph never needed the extra colour. Step 4 is the entire content — for a general cut the restrictions to \(S\) need not be related by a permutation, and exercise 8.1.8 identifies the exact weakening (uniquely \((k-1)\)-colourable) under which the argument still runs.

hconn : G.Connected is load-bearing and is not redundant given hcrit: although IsCritical.connected proves connectivity from criticality, it needs [Nonempty V], which this statement does not assume. Passing hconn explicitly keeps the two results independent and avoids a dependency cycle. Note also that the book’s \(S\)-components are defined only for a connected \(G\), so step 2 genuinely needs it.

Criticality forces the graph to hold together tightly: it can have no single point of failure. Theorem 8.3 goes one step further and analyses the 2-vertex cuts that remain possible — and finds they too are heavily constrained.

There is no IsBlock in Mathlib or this repo, so "is a block" is unfolded into the book’s own definition, connected + no cut vertex. A cut vertex is spelled as a one-element vertex cut, matching IsVertexCut above. The Connected conjunct is not merely decoration: without it the statement would be satisfied by the empty graph.

This is what makes the type 1 / type 2 dichotomy meaningful. Since \(u\) and \(v\) are not joined by an edge, a \((k-1)\)-colouring of a \({u,v}\)-component is free to give them the same colour or different colours; which it is forced to do is exactly the component’s type. Were \(uv\) an edge, every component would be trivially of type 2 and theorem 8.3 would say nothing.

Stated for IsCritical rather than IsKCritical: the book says "\(k\)-critical", but \(k\) plays no role in the argument, so the hypothesis is weakened to plain criticality. huv : u \(\ne \) v is needed to know \({u, v}\) really has two elements.

Many edges force many colours: each colour class is edge-free, so large classes leave too little room for edges. Equality holds exactly for balanced complete multipartite graphs, where every non-edge is inside a class and all classes have the same size.

Stated multiplicatively over \(\mathbb {R}\) — \(\nu ^{2}/(\nu ^{2} - 2\varepsilon )\) would need division and a proof that the denominator is nonzero. (It always is: \(G\) simple gives \(2\varepsilon \le \nu (\nu -1) \lt \nu ^{2}\), so \(\nu ^{2} - 2\varepsilon \ge \nu \gt 0\) whenever \(V\) is nonempty, whence the [Nonempty V] hypothesis.) \(\chi \) is replaced by an arbitrary \(k\) with G.Colorable k, dodging \(\mathbb {N}\infty \); this is equivalent to the book’s statement, since the right-hand side is monotone in \(k\) and \(\chi \) is the least colourable \(k\).

Odd cycles are the sole obstruction to 2-colourability, so if they all pile up on one shortest cycle, only a bounded amount of extra colour is needed to handle them. Minimality in step 2 is what makes the cycle induced, and hence 3-colourable rather than merely small.

The hypothesis quantifies over all pairs of closed walks that are cycles of odd length, and asks for a common support vertex. Note \(h\) is also applied with \(p = q\) in step 2’s minimality argument, where it is vacuous — the content is only in the disjointness contradiction of step 4.

Colour greedily in order of decreasing degree. When the \(i\)-th vertex’s turn comes, two things bound the colours forbidden to it: it has \(d_{i}\) neighbours, so at most \(d_{i}\) colours are blocked; and only \(i - 1\) vertices are coloured so far, so at most \(i - 1\) colours exist. Hence min{d\(_{i}\) + 1, i} colours suffice at step \(i\), and the worst case over \(i\) bounds \(\chi \). This genuinely improves \(\chi \le \Delta + 1\) (corollary 8.1.2): high-degree vertices are handled while few colours exist, low-degree ones later when the count \(i\) no longer binds. Exercise 8.1.4 derives two further bounds from it.

The sorted degree sequence is presented as an equivalence \(\sigma \) : Fin (card V) \(\simeq \) V together with \(h\sigma \), which says i \(\mapsto \) deg (\(\sigma \) i) is antitone — i.e. \(\sigma \) enumerates the vertices in nonincreasing degree order, so G.degree (\(\sigma \) i) is the book’s \(d_{i}\). \(i + 1\) rather than \(i\) because Fin is 0-indexed and the book is 1-indexed.

Worth knowing while filling: \(h\sigma \) is not needed for the proof, only for the statement. Steps 1–4 bound \(\chi \) by that sup for any enumeration \(\sigma \); what \(h\sigma \) buys is that the sup is then the book’s max\(_{i}\) min{d\(_{i}\) + 1, i} for the sorted sequence, which is the small quantity worth having. So do not go looking for a place to use \(h\sigma \) — there isn’t one.

Needing many colours forces many edges: a \(\chi \)-chromatic graph carries at least as many edges as \(K_\chi \). So a sparse graph cannot have a large chromatic number.

The book’s \({x}\) denotes the ceiling, rendered as \(\lceil \cdot \rceil _{+}\) (Nat.ceil), which is the correct choice here since the quantity is nonnegative. Real.sqrt needs a real argument, hence the cast on \(2 * \varepsilon \).

A graph and its complement cannot both be hard to colour: an edge missing from \(G\) is present in \(G^{c}\), so the two compete for the same \(\nu - 1\) adjacencies at each vertex. Equality holds for complete graphs, where \(\chi (K_{n}) = n\) and \(\chi (K_{n}^{c}) = 1\). This is the archetypal Nordhaus–Gaddum inequality, of which many analogues are known for other graph parameters.

The addition is in \(\mathbb {N}\infty \), where subtraction is badly behaved — hence step 1, which moves the whole argument into \(\mathbb {N}\) before any arithmetic. Step 3’s index gymnastics (reverse, then complement) is the fiddliest part and is worth isolating as its own lemma about the two sorted sequences.

\(D\) is the degeneracy of \(G\). Strip off a vertex of degree at most \(D\), repeatedly, recording the order; then colour the vertices back in reverse order — when a vertex is restored it has at most \(D\) neighbours already present, so one of \(D + 1\) colours is free. This refines \(\chi \le \Delta + 1\) (corollary 8.1.2), since \(D \le \Delta \) always and often \(D\) is far smaller: a tree has \(D = 1\), giving \(\chi \le 2\) no matter how large \(\Delta \) is.

"Induced subgraph" is indexed by Finset V (a vertex subset) rather than by a Subgraph, since the book’s maximum is over induced subgraphs only. The sup includes \(s = \emptyset \), whose minDegree is \(0\) by Mathlib’s convention; this can only make \(D\) larger and so weakens the bound harmlessly. Note the induction in step 2 is the formal content of "repeatedly strip off" — as usual, the informal repetition becomes an induction on the size of what remains.

The hypothesis provides some colouring, possibly using far more than \(k\) colours, in which no colour class is a singleton. The claim is that this feature survives optimisation down to \(k\) colours. The difficulty is that the two requirements pull against each other: merging classes reduces the colour count but tends to empty classes out, and the whole point is that it can be arranged never to leave one vertex stranded.

The hypothesis is existential in the number of colours \(n\), so the given colouring is C : G.Coloring (Fin n) for an unknown \(n\) — step 1’s strengthening is what makes that usable. Set.ncard is used rather than a Finset card so the statement needs no decidability on colour classes.

An odd cycle is 3-chromatic and minimally so — delete any edge or vertex and it unrolls into a path, which is 2-colourable. Conversely a 3-critical graph cannot contain an odd cycle properly, and it must contain one, so it is one. This classification is exactly what Brooks’ theorem 8.4 consumes: its proof observes that *since 1-critical and 2-critical graphs are complete and 3-critical graphs are odd cycles, we have \(k \ge 4\)*.

"The only 3-critical graphs are the odd cycles" is up to isomorphism, hence Nonempty (G \(\simeq \)g cycleGraph n) rather than an equality. Steps 3–5 are the same three moves used in isKCritical_two_iff (with an edge in place of an odd cycle); factoring out "a subgraph attaining \(\chi (G)\) must be \(\top \)" as a lemma about IsCritical pays for itself across all three cases of 8.1.7.

A 1-chromatic graph has no edges and at least one vertex. Criticality forces exactly one — with two or more vertices, deleting one leaves a graph still needing one colour, so the chromatic number would not drop.

\(\top \) : SimpleGraph (Fin 1) is \(K_{1}\); on a single vertex the complete and empty graphs coincide, which is what makes step 3 go through despite \(G\) being edgeless. Note that without the Subgraph-lattice definition of IsCritical, step 2 would fail: the edge-only order has no proper subgraph of \(\bot \) to test, and every edgeless graph would count as 1-critical.

A 2-chromatic graph has at least one edge, and a single edge already needs both colours; criticality leaves no room for anything else.

\(\top \) : SimpleGraph (Fin 2) is \(K_{2}\). Step 3 is the shared "a subgraph attaining \(\chi (G)\) must be \(\top \)" lemma noted under the 3-critical case.

This generalises theorem 8.2 from clique cuts to uniquely colourable ones, and isolates what theorem 8.2 was really using. A clique cut forces the vertices of \(S\) to take distinct colours; what the gluing actually needs is only that the partition of \(S\) is forced, so that the pieces can be reconciled by renaming colours. Complete graphs are uniquely colourable, so theorem 8.2 is the special case.

The shared machinery worth extracting once: (i) an \(S\)-component family indexed by ConnectedComponent, (ii) "every edge of \(G\) lies in some \(S\)-component", and (iii) the gluing lemma turning agreement on \(S\) into a colouring of \(G\). With those, theorem 8.2 and this exercise differ only in step 4. \(k - 1\) is \(\mathbb {N}\)-subtraction; hG.1 supplies \(k \ge 1\).

In a critical graph no vertex is redundant, and a vertex whose neighbourhood is contained in another’s is exactly redundant: it can simply inherit that vertex’s colour. Note the argument needs \(u\) and \(v\) nonadjacent to work, and gets it for free — if \(u ~ v\) then \(v \in N(u) \subseteq N(v)\), contradicting looplessness.

Stated with \(\lnot (\dots \subseteq \dots )\), matching the book’s \(\not\subset \). [Nonempty V] is needed to know \(\chi (G) \ge 1\) in step 1.

So \(k\)-critical graphs come in sizes \(k\) (the complete graph \(K_k\)) and \(k + 2\) or more, never \(k + 1\). The reason is that one vertex of slack forces the complement to be a matching, and a matched pair has identical neighbourhoods — the most extreme violation of part (a). Exercise 8.1.12 asks for 4-critical graphs on \(n\) vertices for \(n = 4\) and all \(n \ge 6\); the gap at \(n = 5\) is exactly this result.

Step 2’s degree identity G.degree v + G\(^{c}\).degree v = card V - 1 is the workhorse and is worth stating as its own have. Take care that \(k - 1\) in step 1 is \(\mathbb {N}\)-subtraction — the case \(k = 0\) should be dispatched separately (a 0-chromatic graph has an empty carrier, so card V = 1 is impossible).

No colour can be used on both sides of a join, so the two palettes are forced to be disjoint and the chromatic numbers simply add. This makes joins a convenient way to build graphs of prescribed chromatic number, and is why the wheel \(C_n \lor K_{1}\) needs \(\chi (C_n) + 1\) colours.

Addition is in \(\mathbb {N}\infty \); both summands are finite here (finite carriers), so it is ordinary addition, but the casts still need care — extracting \(a\), \(b\) as naturals up front, as in step 1, keeps the arithmetic in \(\mathbb {N}\). [Nonempty \(\alpha \)], [Nonempty \(\beta \)] ensure both sides genuinely contribute.

By part (a) the join’s chromatic number is the sum, so a drop on one side is a drop for the join. This yields a construction for critical graphs of large chromatic number: join known critical graphs. For instance \(K_{1} \lor C_{5}\) is 4-critical, \(C_{5}\) being 3-critical (exercise 8.1.7) — this is exactly the family exercise 8.1.12 asks for.

Step 4 is the one that would be missed by reasoning only about "remove a vertex or a within-side edge"; the subgraph lattice of a join contains subgraphs that are not themselves joins, and they must be handled.

Glue two \(k\)-critical graphs at a single vertex \(v\), delete one edge at \(v\) from each, and join the two orphaned endpoints \(v_{1}\), \(v_{2}\) by a new edge; the result is again \(k\)-critical. Step 1 is the heart: the new edge forces \(v_{1}\) and \(v_{2}\) apart, so \(v\) must agree with one of them, and that agreement is exactly what repairs the deleted edge on that side. The Hajós construction matters because, iterated from \(K_k\), it generates every graph with chromatic number at least \(k\) — a complete but impractical characterisation.

The outline’s binder \(\{ k\ v\ v_{1}\ v_{2} : \_ \} \) cannot elaborate (heterogeneous types under one hole), so the statement uses explicit \({k : \mathbb {N}} {v v_{1} v_{2} : V}\). Both graphs live on one carrier \(V\); "exactly one vertex in common" is hmeet : G\(_{1}\).support \(\cap \) G\(_{2}\).support = {v}, and each \(G_{i}\)’s real content is G\(_{i}\).induce G\(_{i}\).support, which is why the hypotheses are stated about the induced graphs rather than about \(G_{1}\), \(G_{2}\) directly. Edge deletion is \{} edge and edge addition is \(\sqcup \) edge.

The excluded case \(n = 5\) is exactly exercise 8.1.9(b): no \(k\)-critical graph has \(k + 1\) vertices, so no 4-critical graph has five. The book’s figure 8.2 (the Grötzsch graph) is another witness, for \(n = 11\).

The carrier is pinned to Fin n, so each construction must be transported along an explicit equivalence — Fin 1 \(\oplus \) Fin (n-1) \(\simeq \) Fin n for case 2, and the Hajós single-carrier encoding of exercise 8.1.11 for case 3. That transport, rather than the graph theory, is most of the Lean work here; a reusable "IsKCritical transfers along \(\simeq \)g" lemma is worth having first.

Colour each side separately; the two colourings may clash across the cut, but there are at most \(n - 1\) cut edges and \(n!\) ways to relabel one side’s palette — far more freedom than there are constraints to violate. A thin cut therefore cannot force an extra colour. Note how sharp the count is: \(n\) cut edges would give \(n \cdot (n-1)! = n!\), exactly enough to rule out every permutation.

hcut is stated as #cross + 1 \(\le \) n rather than #cross \(\le \) n - 1 to avoid \(\mathbb {N}\)-subtraction, and it carries \(n \ge 1\) as a side benefit. The partition \((X, Y)\) is \(X\) and its complement, so \(Y\) never appears by name. Step 4 needs Fintype.card (Equiv.Perm (Fin n)) = n ! and the factorial identity \(n ! = n * (n-1)!\).

Criticality forces robust connectivity: a graph that minimally needs \(k\) colours cannot be pulled apart by fewer than \(k - 1\) edge deletions. This sits alongside theorem 8.1, which gives the corresponding degree bound \(\delta \ge k - 1\), and corollary 8.2, which rules out cut vertices — three different senses in which a critical graph is tightly held together.

The conclusion k - 1 \(\le \) edgeConnectivity is the definition of \((k-1)\)-edge-connected (B&M §3.1: \(G\) is \(k\)-edge-connected if \(\kappa ' \ge k\)), so no separate predicate is needed. Step 1 relies on sInf \(\emptyset \) = 0 being harmless: if \(G\) has no edge cut at all the bound must still be proved, and there step 2 has nothing to work with — dispatch that case by noting a graph with no edge cut is complete or trivial.

Corollary 8.1.2 gives \(\chi \le \Delta + 1\) for every graph; Brooks says only two families attain it — odd cycles (\(\chi = 3 = \Delta + 1\)) and complete graphs (\(\chi = n = \Delta + 1\)). Everything else needs only \(\Delta \) colours. The book contrasts this with Vizing’s theorem 6.2, where many graphs satisfy \(\chi ' = \Delta + 1\). The trick of the proof is the ordering: by ending at a vertex two of whose neighbours were forced to share a colour, the greedy algorithm is given one unit of slack exactly where it would otherwise run out.

0 hits in Mathlib — this is a genuine build. hnotcycle is stated as \(\forall \) n, Odd n \(\to \) IsEmpty (G \(\simeq \)g cycleGraph n), i.e. \(G\) is isomorphic to no odd cycle; hnotcomplete as \(G \ne \top \). Both are consumed only in step 2. Step 1’s caveat is worth taking seriously before starting: the reduction to the critical subgraph is stated casually by the book but is not free in Lean.

Theorem 8.1 already gives \(2\varepsilon \ge \nu (k-1)\) for a \(k\)-critical graph; the exercise’s content is the extra \(+1\), which says the bound is never exactly attained — not every vertex can have degree exactly \(k - 1\). That is precisely Brooks in disguise: a \((k-1)\)-regular critical graph would have \(\chi = k = \Delta + 1\), which Brooks forbids outside the two exceptional families.

Both sides are pinned to Type (not Type*) so that the two quantifications range over the same universe and the \(\leftrightarrow \) is well-formed. Note the statement quantifies over graphs, so each direction instantiates the assumed side at a graph it constructs — this is an equivalence of schemas, not of propositions about one fixed \(G\).

The edge chromatic number \(\chi '(G)\) is the chromatic number of the line graph \(L(G)\), whose vertices are the edges of \(G\) with adjacency "shares an end". So Brooks’ vertex-colouring theorem yields an edge-colouring bound, recovering for cubic graphs what Vizing’s theorem 6.2 gives in general.

Two departures from the book, both weakenings. (i) \(\chi '\) is spelled as \(\chi \)(lineGraph); there is no separate chromaticIndex here. (ii) The book says loopless, which in B&M permits parallel edges; SimpleGraph has none, so this is the simple-graph case only. With multiplicities the degree count in step 1 is unchanged, but lineGraph would have to be redefined, so the weakening is deliberate. Note also that the exercise is stated with \(\Delta = 3\) exactly, not \(\Delta \le 3\); only \(\le \) is used.

At a 2-vertex cut a critical graph splits into exactly two pieces with opposite demands on \(u\) and \(v\) — one insisting they agree, the other that they differ. That is why the cut cannot be repaired, and it is the structural fact that both Brooks’ theorem (via corollary 8.3) and theorem 8.5 exploit.

Worth proving first, and reused in step 6: for \(k \ge 2\), criticality can be checked on single-edge deletions alone. Any \(H \lt \top \) is contained in some \(\top \) \{} edge e, and \(\chi \) is monotone, so \(\chi \)(H.coe) \(\le \) \(\chi \)(\(\top \) \{} edge e); vertex deletions are subsumed because a critical graph has \(\delta \ge k - 1 \ge 1\) (theorem 8.1), so every vertex carries an edge. This closes the gap between the book’s edge-only check and the Subgraph-lattice definition of IsCritical.

The (by simp [uvComponent]) arguments in the statement are the membership proofs u, v \(\in \) (uvComponent …).verts, discharged by unfolding — the \({u, v}\) is glued onto every component by construction.

This inequality is precisely what Brooks’ theorem uses to dispose of the 2-vertex-cut case: combined with \(d(u), d(v) \le \Delta \) it forces \(2\Delta \ge 3k - 5\), which for \(k \ge 4\) already gives \(k \le \Delta \).

Stated additively as \(3k \le d(u) + d(v) + 5\) rather than \(d(u) + d(v) \ge 3k - 5\), because \(\mathbb {N}\)-subtraction would truncate \(3k - 5\) to \(0\) for \(k \le 1\) and make the statement vacuous exactly where it should be informative. Step 5 deserves care: if \(u\) and \(v\) had a common neighbour in \(G_{2}\), contracting would merge two edges into one and the degree identity would fail — establish that they do not, or weaken the identity to the inequality actually needed.

This is the case \(k = 4\) of Hajós’ conjecture, settled by Dirac (1952). The book notes the conjecture in general is *known to be a very difficult problem*, and mentions Hadwiger’s related conjecture, whose case \(k = 5\) Wagner showed equivalent to the four-colour conjecture of chapter 9.

Step 1’s monotonicity lemma is what licenses the book’s "without loss of generality" and should be built first — without it the reduction to the critical subgraph is not available. The induction in step 2 is on the carrier’s cardinality, but cases A and B produce graphs on different carriers (subgraph coercions), so the induction is cleanest stated over all graphs on all carriers of bounded size rather than over subgraphs of a fixed \(G\).

Essentially-all vertices having degree at least three is enough to force a topological \(K_{4}\), with no colouring hypothesis at all. So this is a purely degree-theoretic sufficient condition where theorem 8.5 gives a chromatic one. Neither is necessary: a subdivision of \(K_{4}\) can occur in graphs that are only 3-chromatic — the book’s own example, a 4-cycle being a subdivision of \(K_{3}\), makes the analogous point one dimension down.

"At most one vertex of degree less than three" is a Finset cardinality bound on univ.filter (fun v => G.degree v < 3). This is the statement exercise 8.3.2(a) reduces to, so filling that one first is not an option — the dependency runs this way.

Enough edges relative to vertices force the graph to be locally rich enough to contain four branch vertices and six connecting paths. The invariant in step 2 is the whole trick: deleting a low-degree vertex is "free" with respect to the quantity \(2\nu - \varepsilon \), so the stripping can be run to completion without ever losing the hypothesis. Part (b) shows \(2\nu - 2\) is exactly the right threshold.

Restated additively as \(2\nu \le \varepsilon + 2\) rather than \(\varepsilon \ge 2\nu - 2\), to keep \(\mathbb {N}\)-subtraction out. Step 2’s bookkeeping is the \(\mathbb {N}\)-arithmetic core and is worth isolating: (G.induce {v}\(^{c}\)).edgeFinset.card + G.degree v = G.edgeFinset.card.

Classify the \(k\)-colourings of \(G - e\) by whether they give \(u\) and \(v\) the same colour: the "same" ones are the colourings of \(G \cdot e\), the "different" ones are the colourings of \(G\). The book notes the recursion *bears a close resemblance to the recursion formula for \(\tau (G)\)* in theorem 2.8, and that it can be run in either direction — reducing to empty graphs (efficient for sparse \(G\)) or to complete graphs (efficient for dense \(G\)), as illustrated in figure 8.9.

Stated additively, \(\pi _k(G) + \pi _k(G\cdot e) = \pi _k(G-e)\), to stay in \(\mathbb {N}\) — the book’s headline form has a subtraction. Happily this is how B&M’s own proof ends, so the Lean statement is the more faithful of the two. Steps 2 and 3 are the only real work; step 1 is bookkeeping and step 4 is \(rw\).

This is what justifies calling \(\pi _k(G)\) the chromatic polynomial. The book notes that no one has yet discovered which polynomials are chromatic: Read (1968) conjectured the coefficients must first rise then fall in absolute value, but even that plus this corollary is not sufficient — \(k^{4} - 3k^{3} + 3k^{2}\) satisfies all of them yet is no graph’s chromatic polynomial (exercise 8.4.2(b)).

[Nonempty V] is load-bearing, as step 2 shows: for \(\nu = 0\) the empty graph has \(\pi _k = 1\), whose constant term is \(1\), not \(0\). The alternation is encoded as \(\forall \) i, 0 \(\le \) (-1)^(\(\nu \) - i) * p.coeff i rather than as an explicit sum with non-negative \(a_{i}\), which is equivalent and much easier to carry through step 5.

The second coefficient of the chromatic polynomial simply counts the edges. The mechanism is that each deletion–contraction step peels off exactly one copy of the contracted graph’s leading term, and the contracted graph has degree one less — so the \(k^{\nu -1}\) coefficient decrements once per edge. This is a first small step toward the general question of which polynomials are chromatic, and it is what makes exercise 8.4.2(b) possible.

\(p\) is a hypothesis rather than a construction, which is why step 1 is needed at all — without uniqueness there is no link between the \(p\) given here and the one corollary 8.6 builds. That uniqueness lemma is worth stating once and reusing in exercises 8.4.2(b) and 8.4.8.

Root the tree anywhere and colour outward: the root takes any of the \(k\) colours, and every other vertex is reached across exactly one edge from its already-coloured parent, so it avoids just that one colour. The formula reflects the structure exactly — \(\nu - 1\) edges, each imposing precisely one constraint, with no cycles to make the constraints interact.

\((k - 1)\) is \(\mathbb {N}\)-subtraction, harmless because at \(k = 0\) both sides are \(0\) for a nonempty tree. Consumed by exercises 8.4.3(b) (as the spanning tree bound) and 8.4.4 (as the deleted-edge case of the cycle).

Among connected graphs on \(\nu \) vertices, trees are exactly the ones with the most colourings: every extra edge kills at least one colouring of the spanning tree.

The two clauses are bundled as a conjunction because the book states them together; only the second needs the guard on \(k\). Note step 5 is where the whole content sits — step 2’s inequality is nearly formal.

Sanity checks: at \(k = 2\) the formula gives \(1 + (-1)^{n}\), which is \(2\) for even \(n\) and \(0\) for odd \(n\) — matching that even cycles are bipartite (two 2-colourings) and odd cycles are not (none). The \((-1)^{n}\) term is precisely where the parity of the cycle enters, and it is what makes odd cycles the exceptional family throughout this chapter.

Stated over \(\mathbb {Z}\) with a cast on the left, because \((k-1)^{n} + (-1)^{n}(k-1)\) is not a natural number expression — the \((-1)^{n}\) term is genuinely negative for odd \(n\). The base case is \(n = 3\) rather than \(n = 0\) because cycleGraph n is only a cycle for \(n \ge 3\), and because contracting an edge of \(C_{3}\) would leave a multi-edge, which contractEdge silently simplifies.

Choose the apex’s colour first — \(k\) ways — and then \(G\) must be coloured with the remaining \(k - 1\) colours. This is the chromatic-polynomial counterpart of \(\chi (G \lor K_{1}) = \chi (G) + 1\), the \(K_{1}\) case of exercise 8.1.10(a).

\(hk : 1 \le k\) keeps \(k - 1\) from truncating in step 3, where the equivalence {c : Fin k // c \(\ne \) j} \(\simeq \) Fin (k-1) genuinely needs \(k \ge 1\). The statement happens to hold at \(k = 0\) as well — both sides are then \(0\), the join being nonempty — so \(hk\) is a convenience for the proof rather than a correction to the claim.

A wheel with \(n\) spokes is \(C_n \lor K_{1}\) — a rim cycle plus a hub joined to every rim vertex — so its colourings are a hub colour together with a colouring of the rim in the remaining palette. Sanity check: at \(k = 3\) and odd \(n\) the formula gives \(3\cdot 1 + (-1)\cdot 3\cdot 1 = 0\), matching that a wheel with an odd rim is 4-chromatic and so has no 3-colouring at all.

\(hn : 3 \le n\) is inherited from exercise 8.4.4 (the rim must be a genuine cycle); \(hk : 1 \le k\) is what step 4 consumes.

No edge joins different components, so their colourings are entirely independent: a colouring of \(G\) is precisely a choice of colouring for each component, and the count multiplies. This is the chromatic-polynomial version of \(\chi \)(G) = max \(\chi \)(G\(_{i}\)), and one of the formulae the book lists as *facilitating the calculation of chromatic polynomials*.

Step 2 is the same "components are independent" equivalence used by IsCritical.connected (in its sup form) — worth building once in a shared place and specialising twice, since the counting and the \(\chi \) versions differ only in what is applied to the resulting family.

A gluing formula. A colouring of the union is a pair of colourings of the parts agreeing on the overlap; because the overlap is complete, its vertices must take distinct colours, which makes the two sides’ colourings matchable in a uniform number of ways. Together with exercise 8.4.6 (components multiply) this is one of the practical tools for computing chromatic polynomials by decomposition.

Phrased on the Subgraph lattice — \(\sqcup \) and \(\sqcap \) of G.Subgraph — because SimpleGraph V has no notion of union/intersection with differing vertex sets. hcomp : (G’ \(\sqcap \) H’).coe = \(\top \) says the overlap is complete *as a graph on its own vertex set*. Note that the book’s identity is stated multiplicatively precisely to avoid the division that step 5 also avoids.

\(\pi _k(G)\) counts colourings, so it is positive at every integer \(k \ge \chi (G)\), and \(\chi (G) \le \nu \) always. The exercise strengthens this from integers to all reals: beyond \(\nu \) the polynomial has no zero whatsoever. The book notes that the roots of chromatic polynomials exhibit an unexpected regularity for planar graphs, citing Tutte (1970) on their connection with the golden ratio.

Over \(\mathbb {R}\) here (not \(\mathbb {Z}\) as in corollary 8.6), since the claim is about real roots; \(hp\) ties \(p\) to the integer-valued counting function at naturals only, which is exactly what step 1 needs. Step 2 is the substantial piece and is of independent interest — it is the standard proof that \(\pi _k\) is a polynomial at all, and an alternative to corollary 8.6’s induction.

One might expect a graph needing many colours to contain a large clique — after all, a clique’s vertices must all differ. This theorem says the converse fails badly: chromatic number can be arbitrarily high with no triangle at all. Starting from \(K_{2}\), the construction gives a triangle-free \(k\)-chromatic graph on \(3\cdot 2^{k-2} - 1\) vertices — the 5-cycle for \(k = 3\), the Grötzsch graph for \(k = 4\). The book adds that Erdős (1961) proved by the probabilistic method that for any \(k, l \ge 2\) there is a graph of girth \(k\) and chromatic number \(l\), and that Descartes’ construction (exercise 8.5.2) already achieves girth \(6\).

Self-contained: everything needed is the local mycielskian def, and step 5’s recolouring is the only delicate part. The carrier is existentially quantified, so each induction step may change it — which is exactly what mycielskian does (W \(\mapsto \) W \(\oplus \) W \(\oplus \) Unit). Note the "without loss of generality" in the book’s step 5 is a genuine permutation of the palette and must be performed explicitly.

Theorem 8.7 already shows \(G_k\) is \(k\)-chromatic; the exercise asks for the stronger fact that it is minimally so — the shadows and apex are arranged so tightly that every element of the graph is load-bearing. So the Mycielski tower produces not just triangle-free graphs of high chromatic number but triangle-free critical ones. For \(k = 3\) it gives the 5-cycle (3-critical by exercise 8.1.7) and for \(k = 4\) the Grötzsch graph, which the book displays in figure 8.2 precisely as its example of a 4-critical graph.

mycielskiTower is Sigma-valued, so (mycielskiTower k).2 is the graph and (mycielskiTower k).1 its carrier; the induction in step 1 must therefore be stated over the Sigma, not over a fixed carrier. The definitional unfolding mycielskiTower (k+1) = ⟨_, (mycielskiTower k).2.mycielskian⟩ is what makes step 2 usable.

Mycielski’s construction (theorem 8.7) removes triangles but still leaves 5-cycles. Descartes’ construction is stronger — it keeps the girth at six or more, so the graphs have no short cycles at all, and yet the chromatic number still climbs without bound. Blanche Descartes (1954) gave the original recursive construction; the book calls Mycielski’s the easier one, which is why §8.5 proves theorem 8.7 in the text and relegates this to a starred exercise.

The conclusion is \(\ge k + 1\), not \(= k + 1\): the construction gives a lower bound and the exercise asks only for that. Likewise 6 \(\le \) girth rather than \(= 6\). Step 1 is most of the Lean work — the indexed family of copies and the per-copy matching bijection have to be built explicitly, and Fintype instances derived for the resulting carrier.

High chromatic number is compatible not merely with triangle-freeness (theorem 8.7) but with the complete absence of short cycles. Locally such a graph looks like a tree — every small neighbourhood is acyclic and trivially 2-colourable — yet globally it resists any bounded number of colours. Chromatic number is a genuinely global invariant.

The conclusion is the honest \(\ge \) form (\(k \le \chi \), 6 \(\le \) girth) rather than the book’s "\(k\)-chromatic of girth six". Two reasons: part (a) delivers only a lower bound on \(\chi \), and girth = 6 exactly would additionally require exhibiting a 6-cycle, which the construction does not obviously do. Step 3’s instantiation at \(m\) rather than \(k\) is the small manoeuvre that lets the \(\ge \) induction feed part (a)’s \(=\) hypothesis.

Greedily enlarge the first colour class to a maximal independent set, absorbing whatever later classes will give up; repeat on what remains. Nothing is lost: the result is canonical and uses no more colours than before.

Why this matters (§8.6). The storage problem asks for the fewest warehouse compartments so that incompatible chemicals are separated — which is the chromatic number of the incompatibility graph. No good algorithm is known, so the book gives an enumerative procedure: list the minimal coverings (equivalently, by theorem 7.1, the maximal independent sets), then search over canonical colourings. This exercise is what makes that search complete — restricting attention to canonical colourings loses nothing. The book’s example (figure 8.11) has minimal coverings \({a,c,e,g}\), \({b,c,d,e,g}\), \({b,d,e,f}\), \({b,c,d,f}\), hence maximal independent sets \({b,d,f}\), \({a,f}\), \({a,c,g}\), \({a,e,g}\), and \(\chi = 3\) via the canonical colouring \(({b,d,f}, {a,e,g}, {c})\).

L.length \(\le \) k, not \(= k\): a canonical colouring may use fewer colours than the one it was built from, and that is precisely the point — the least length over canonical colourings is \(\chi (G)\), which is what the §8.6 procedure computes. Step 1’s strengthening is essential: the statement as given is not directly inductive, because the recursive call is about a deleted graph.