Take \(v\) of maximum degree \(\Delta \). All \(\Delta \) edges at \(v\) are pairwise adjacent, so a proper colouring gives them \(\Delta \) distinct colours.

\(\chi '\) is G.lineGraph.chromaticNumber, valued in \(\mathbb {N}\infty \), so \(\Delta \) is cast.

This bound is half of every result in the chapter: Theorem 6.1 says bipartite graphs attain it, Vizing says nobody exceeds it by more than one.

\(c(v)\) counts distinct colours on the \(d(v)\) edges at \(v\); distinct colours cannot outnumber the edges carrying them. Strict exactly when two edges at \(v\) repeat a colour.

Two edges are adjacent exactly when they meet at a vertex, so "no two adjacent edges share a colour" is "at every vertex the incident edges carry distinct colours" — i.e. \(c(v) = d(v)\).

Properness is stated directly as \(\forall \) e\(_{1}\) e\(_{2}\), G.lineGraph.Adj e\(_{1}\) e\(_{2}\) \(\to \) C e\(_{1}\) \(\ne \) C e\(_{2}\) rather than by packaging \(C\) as a lineGraph.Coloring, since \(C\) here is a bare function.

This equivalence is the bridge turning "make the colouring proper" into the numerical goal "maximise \(\sum _v c(v)\)", which is what optimality is about.

An Euler tour threads through every vertex; alternating colours along it means any vertex with room for two edges sees both. Odd cycles are the sole exception, since alternation around an odd cycle must repeat somewhere.

! "is not an odd cycle" is a statement about \(G\) itself, not about containing one. Hence the clause p.edges.toFinset = G.edgeFinset in hnotodd is load-bearing: it says the cycle exhausts \(G\). Dropping it would make the hypothesis far too strong (excluding every graph with an odd cycle anywhere) and the lemma useless for Lemma 6.1.2, which applies it to two-coloured components.

A wasted colour at \(u\) — one missing, another doubled — is an opportunity to improve; the only structure blocking the repair is an odd cycle, whose alternation cannot work out.

! "represented at least twice at \(u\)" counts edges, not colours, so \(hj\) is 2 \(\le \) (univ.filter fun e => ↑e \(\in \) G.incidenceSet u \(\land \) C e = j).card rather than anything phrased via numColoursAt.

! The conclusion "the component is an odd cycle" is stated as: there is an odd cycle \(p\) at \(u\) in twoColourSubgraph C i j whose support coincides with the component’s supp. The membership form \(\forall \) w, w \(\in \) p.support \(\leftrightarrow \) w \(\in \) (…).supp is used instead of a set equality to avoid a Fintype (ConnectedComponent.supp) obligation that does not synthesize.

Contrapositive: if \(\chi ' \gt \Delta \), an optimal \(\Delta \)-colouring cannot be proper, so by (6.3) some \(u\) has \(c(u) \lt d(u)\) — a colour missing while another repeats. That is Lemma 6.1.2’s hypothesis, which forces an odd cycle, so \(G\) is not bipartite.

! The book’s "Clearly, \(u\) satisfies the hypothesis of lemma 6.1.2" compresses a real step. From \(c(u) \lt d(u)\) one gets some colour repeated at \(u\); getting a colour not represented at \(u\) needs the pigeonhole \(c(u) \lt d(u) \le \Delta \) — i.e. that only \(\Delta \) colours are available and fewer than \(d(u)\) are used. With \(d(u) \le \Delta \) this is tight and worth isolating.

! The odd cycle produced by Lemma 6.1.2 lives in twoColourSubgraph C i j, a subgraph of \(G\). Transporting it to an odd cycle of \(G\) (to contradict bipartiteness) requires a walk-level map along twoColourSubgraph \(\le \) G, which is not stated in this file.

By (6.1) \(\chi ' \ge \Delta \) always, so the content is that one spare colour suffices — a tight dichotomy in which no simple graph needs \(\Delta + 2\).

The disjunction is stated with the two branches at different types ((G.maxDegree : \(\mathbb {N}\infty \)) and (G.maxDegree + 1 : \(\mathbb {N}\)) coerced), which is harmless but worth matching carefully when proving.

The half of Vizing that carries all the work. With (6.1) supplying \(\chi ' \ge \Delta \), the two together pin \(\chi '\) into \({\Delta , \Delta +1}\).

Swapping roles along \(P\) moves exactly one edge from the larger matching to the smaller, leaving the union unchanged. Repeated application balances a family of matchings — in §6.3’s timetabling reading, spreading lessons evenly across periods so fewer classrooms are needed at once.

\(|M'| = |M| - 1\) is stated additively as M’.ncard + 1 = M.ncard to avoid \(\mathbb {N}\) subtraction.

Matchings are carried as Set (Sym2 V) together with an existential witness \(\exists \) S : G.Subgraph, S.IsMatching \(\land \) S.edgeSet = M, rather than as subgraphs directly — which makes the set operations \(\setminus \), \(\cup \) in the book’s formulas literal, at the cost of re-deriving the subgraph witness for \(M'\) and \(N'\).

! In the book’s notation \([x]\) is the floor and \({x}\) the ceiling — the opposite of the modern convention for \({}\). So (6.5) reads \(\lfloor \varepsilon /p\rfloor \le |M_{i}| \le \lceil \varepsilon /p\rceil \), rendered here as G.edgeFinset.card / p \(\le \) …\(\le \) (G.edgeFinset.card + p - 1) / p in \(\mathbb {N}\) division.

! The book’s "repeatedly applying lemma 6.3 ... we eventually obtain" is an induction whose termination is not argued. In Lean it needs an explicit measure — e.g. \(\sum _{i} |M_{i}|^{2}\), which strictly decreases on each rebalancing since moving an edge from a larger to a smaller class reduces the sum of squares. Supplying that measure is a real part of the formalisation the book skips.

Pad until every vertex has degree exactly \(\Delta \). Enlarge the smaller side with isolated vertices so the sides match; then repeatedly join a deficient vertex on each side — both sides have equal total deficiency, so such a pair always exists.

! Carrier changes, so the statement produces a new type \(W\) together with an embedding \(G \hookrightarrow g H\).

! The \(\hookrightarrow g\) here is a RelEmbedding, i.e. an induced embedding — the same trap that sank the original statement of exercise 1.4.1 in GraphsAndSubgraphs.lean (recorded in GraphTheory/ExtractionArchive/MathlibDuplicates.md, entry 5). It demands H.Adj (f a) (f b) \(\leftrightarrow \) G.Adj a b, so the padding edges must never join two images of \(G\)-vertices. The two-disjoint-copies construction respects this; the naive "add edges between deficient vertices of \(G\) itself" does not, and would make the statement false. Worth checking carefully before proving.

Part (b) is the alternative proof of Theorem 6.1: a \(\Delta \)-regular bipartite graph is 1-factorable (exercise 5.2.3(a)), hence properly \(\Delta \)-edge colourable, and restricting to \(G\) gives \(\chi '(G) \le \Delta \).

+ This route avoids Lemma 6.1.1 and the Euler theorem entirely, so it is the recommended path to Theorem 6.1 in Lean — see the note there.

The dual of proper colouring. Proper asks that no colour appear twice at a vertex, using \(\Delta \) colours; this asks that every colour appear at least once at every vertex, using \(\delta \) colours. Since the least degree is \(\delta \), that is the most one could force everywhere.

The colouring is explicitly not required to be proper, so the statement is about IsRepresentedAt rather than about lineGraph.chromaticNumber — one of the few places the raw-function encoding is the right one.

Exercise 6.2.8 is the simple-graph analogue with \(\delta - 1\) colours; it is not stated in this file.

\(K_{2n-1}\) has odd order, so no colour class is a perfect matching and each misses a vertex. With \(\varepsilon = (2n-1)(n-1)\) and classes of size \(\le n - 1\), at least \(2n - 1\) colours are needed — one more than \(\Delta = 2n - 2\). So odd complete graphs sit on the upper side of Vizing’s dichotomy.

The explicit colouring: place the vertices at the corners of a regular \((2n-1)\)-gon and colour each edge by the axis of symmetry it is perpendicular to. Each class is a matching of \(n - 1\) edges missing one vertex, and there are \(2n - 1\) axes.

Concretely in ZMod (2n-1): colour \(s(a, b)\) by \(a + b\). Two edges at a shared vertex get different sums because \(2\) is invertible mod an odd number — which is exactly where oddness enters.

\(K_{2n}\) has \(\Delta = 2n - 1\), so (6.1) gives \(\chi ' \ge 2n - 1\). For the upper bound use the round-robin schedule of exercise 5.1.5(a)(i): the edges partition into \(2n - 1\) perfect matchings, and colouring each with its own colour is proper. So \(\chi ' = \Delta \) and even complete graphs sit on the lower side of the dichotomy.

The contrast with the odd case is entirely parity: with an odd number of vertices no round can involve everybody.

Each colour class is a matching, and a matching on an odd number of vertices misses one, so has \(\le (\nu -1)/2\) edges. A \(k\)-regular graph has \(\varepsilon = k\nu /2\), and a proper \(k\)-colouring would need \(k\nu /2 \le k(\nu -1)/2\) — false. So \(\Delta = k\) colours do not suffice, and Vizing gives exactly one more.

Generalises the odd complete graph of exercise 6.2.1: regularity plus odd order always forces the upper class.

With \(\nu = 2n + 1\) odd, every matching covers an even number of vertices so has \(\le n\) edges. A proper \(\Delta \)-colouring accounts for at most \(n\Delta \) edges; \(h\varepsilon \) says there are more, so \(\Delta \) colours cannot suffice and Vizing supplies exactly one more.

+ The reusable engine of §6.2’s exercises — 6.2.2, 6.2.3(b)(i) and 6.2.3(b)(ii) all reduce to it. Worth proving first among them.

Start from \(k\)-regular on \(2n\) vertices, \(\varepsilon = kn\). Subdividing inserts a degree-\(2\) vertex: \(2n + 1\) vertices — now odd — and \(kn + 1\) edges, with \(\Delta \) still \(k\) provided \(k \ge 2\). Part (a) then applies since \(kn + 1 \gt kn = n\Delta \).

A single subdivision flips the parity of the vertex count and pushes the graph from the lower to the upper side of Vizing’s dichotomy.

! \(hk : 2 \le k\) is load-bearing: at \(k = 1\) the new degree-\(2\) vertex would raise \(\Delta \) to \(2\), and the count \(n\Delta \) would change with it, breaking the application of part (a).

An odd-order \(k\)-regular graph on \(2n + 1\) vertices has \(\varepsilon = k(2n+1)/2\) and \(\Delta = k\). Deleting fewer than \(k/2\) edges cannot lower \(\Delta \), and leaves the count above \(nk\), so part (a) applies.

Odd-order regular graphs stay firmly in the upper Vizing class under small perturbation: at least \(k/2\) edges must go before the conclusion can fail.

\(|F| \lt k/2\) is stated as 2 * F.card < k to avoid \(\mathbb {N}\) division.

In a cubic graph a proper 3-edge colouring splits the edges into three perfect matchings. Any two of them form a spanning 2-regular subgraph — a disjoint union of even cycles. If that union had more than one cycle, swapping the two colours around a single cycle would give a genuinely different partition, contradicting uniqueness. So each pair of classes is a single spanning cycle, i.e. a Hamilton cycle.

! hcol is mandatory. IsUniquelyEdgeColourable quantifies over proper 3-colourings; if none exists the condition holds vacuously, and the statement would then assert that every cubic graph with no 3-edge-colouring is hamiltonian — false, the Petersen graph being a counterexample (\(\chi ' = 4\), nonhamiltonian). Requiring G.lineGraph.Colorable 3 rules that out.

The book’s "product" is exactly Mathlib’s boxProd, written \(\square \).

\(G \square K_{2}\) is two disjoint copies of \(G\) plus a perfect matching joining corresponding vertices, so every degree rises by one and \(\Delta (G \square K_{2}) = \Delta (G) + 1\).

Vizing gives \(G\) a proper \((\Delta (G)+1)\)-colouring. Use it on both copies, then colour the connecting matching edges by recycling — each vertex of a copy already omits at least one of the \(\Delta (G)+1\) colours, and the two copies can be arranged to omit different ones, so each matching edge finds a free colour.

\(G \square H\) has degree \(d(u) + d(v)\) at \((u, v)\), so \(\Delta (G \square H) = \Delta (G) + \Delta (H)\). Decompose \(H\) into \(\Delta (H)\) matchings via its optimal colouring; each matching crossed with \(G\) reproduces part (a)’s situation, and assembling gives \(\Delta (G) + \Delta (H)\) colours.

So the class attaining \(\chi ' = \Delta \) is closed under products with any nontrivial member — one of the few general constructions guaranteeing the lower Vizing class.

\(H\) nontrivial is 0 < H.maxDegree; without it \(H\) is edgeless, \(G \square H\) is a disjoint union of copies of \(G\), and the claim reduces to \(\chi '(G) = \Delta (G)\) which need not hold.