Every visit to a vertex consumes one edge coming in and one going out, so the edges at each vertex must pair up.

The (\(\Leftarrow \)) direction is a minimal counterexample argument. In Lean that is strong induction on \(\varepsilon (G)\) — the book’s "choose such a graph with as few edges as possible" — generalised over the graph, since \(G'\) is a different graph on (the subtype of) the same vertex type.

By Corollary 1.1 the number of odd-degree vertices is always even, so "at most two" means exactly \(0\) or \(2\).

This is the precise answer to the Königsberg question and to exercise 4.1.1: a figure can be drawn "without lifting the pen and without retracing" exactly when it is connected and has at most two odd-degree vertices.

A hamiltonian graph is held together by a single cycle through every vertex, and a cycle is hard to shatter: removing \(k\) vertices from it leaves at most \(k\) arcs.

\(G - S\) is rendered as ((\(\top \) : G.Subgraph).deleteVerts ↑S).coe, so the component count is Nat.card of that graph’s ConnectedComponent. Using the Subgraph API rather than G.induce (↑S)\(^{c}\) is what lets the "spanning subgraph" step be stated at all, since \(C - S\) and \(G - S\) then live over the same vertex set.

If every vertex is joined to at least half the graph, there is enough adjacency that a spanning cycle cannot be avoided.

\(\delta \ge \nu /2\) is formalised as \(\nu \le 2\delta \) to stay in the natural numbers and avoid the rounding ambiguity of \(\nu /2\) under truncated division.

The book’s proof is two sentences only because it reuses the \(S\)/\(T\) counting argument (4.4) from Theorem 4.3. In Lean that argument has to exist somewhere concrete — so this lemma, not Dirac, is the right place to write it out, and Dirac then follows from the closure machinery.

Expanded, (4.4) is: from a Hamilton cycle of \(G + uv\) that must use \(uv\), extract a Hamilton path \(v_{1} \dots v_\nu \) in \(G\) with \(v_{1} = u\), \(v_\nu = v\). Put \(S = {v_{i} | u ~ v_{i+1}}\) and \(T = {v_{i} | v_{i} ~ v}\). Then \(v_\nu \notin S \cup T\) gives \(|S \cup T| \lt \nu \), and \(S \cap T = \emptyset \) because a common \(v_{i}\) would close the Hamilton cycle \(v_{1} \dots v_{i} v_\nu v_{\nu -1} \dots v_{i+1} v_{1}\) in \(G\). Hence \(d(u) + d(v) = |S| + |T| \lt \nu \).

Stated in the file’s "honest restatement" form: instead of positing a closure operator, it says that if \(H\) is reachable from \(G\) by any finite chain of ClosureSteps, then \(G\) is hamiltonian exactly when \(H\) is. Taking \(H\) to admit no further step recovers the book’s statement.

This restatement is what lets the file skip Lemma 4.4.2 entirely — see below.

The book must prove \(c(G)\) well defined before Theorem 4.4 can even be stated; its proof (§4.2, p. 64) is the argument:

Because this file quantifies over ReflTransGen ClosureStep chains rather than naming a closure, Lemma 4.4.2 is not needed and is not formalised: the statement above holds for every chain, confluent or not. It would only be required if a closure : SimpleGraph V \(\to \) SimpleGraph V function were introduced.

Stated with \(\top \) in place of "\(c(G)\) is complete", and ClosureStep reachability in place of the closure operator.

In \(K_{n}\) every pair of distinct vertices is adjacent, so any enumeration \(v_{1} v_{2} \dots v_n v_{1}\) is already a Hamilton cycle. Three vertices are needed because a cycle must have length at least three — \(K_{1}\) and \(K_{2}\) have no cycle at all.

! Despite the book calling it "trivial", Mathlib has no such lemma, and it is not trivial in Lean: it requires exhibiting a concrete cyclic enumeration of \(V\) and proving the resulting walk is a cycle whose support is nodup and spans.

! The hypothesis is formalised in counting form, not by indexing the sorted degree sequence. The book’s \(d_m \le m\) says "at least \(m\) vertices have degree \(\le m\)", and \(d_{\nu -m} \lt \nu - m\) says "at least \(\nu - m\) vertices have degree \(\lt \nu - m\)" — precisely the two Finset.filter cardinalities in hcond. This avoids all \(1\)- versus \(0\)-indexing hazards around degreeSequence, at the cost of no longer looking like the book’s inequality.

The book’s \(m \lt \nu /2\) is written \(2 * m \lt \nu \), and \(m \ge 1\) is made explicit (the book’s \(m\) is a degree \(d'(u)\), and \(m = 0\) is excluded by connectivity considerations implicit in "as large as possible").

The family \({C_{m,\nu }}\) consists of the degree-maximal nonhamiltonian graphs: any nonhamiltonian graph has degrees dominated, position by position, by one of them.

Corollary 4.6 — bounding the edge count of a nonhamiltonian graph reduces to computing \(\varepsilon (C_{m,\nu })\).

Enough edges guarantee a spanning cycle, and this pins down exactly how many "enough" is: a nonhamiltonian graph has at most \(C(\nu -1, 2) + 1\) edges.

"By theorem 1.1" is the handshaking lemma — degree majorisation transfers to an edge-count inequality because \(2\varepsilon = \sum d(v)\).

! The book’s algebra is over \(\mathbb {Q}\) (note the \(\tfrac {1}{2}\)); in \(\mathbb {N}\) the identity \(\tfrac {1}{2}(m^{2} + (\nu -2m)(\nu -m-1) + m(\nu -1)) = C(\nu -1,2) + 1 - \tfrac {1}{2}(m-1)(m-2) - (m-1)(\nu -2m-1)\) involves subtraction that truncates. Either clear denominators and work with \(2\varepsilon \) throughout, or cast to \(\mathbb {Z}\)/\(\mathbb {Q}\) for the identity and cast back. The latter is likely cleaner.

The equality analysis of the first half. The final inequality is tight only when both subtracted terms \(\tfrac {1}{2}(m-1)(m-2)\) and \((m-1)(\nu -2m-1)\) vanish, which happens only for \(m = 1\), or \(m = 2\) together with \(\nu = 5\).

So the bound is attained by exactly one graph for each \(\nu \), plus one sporadic extra at \(\nu = 5\): the densest nonhamiltonian simple graphs there are.

! The book’s closing "which is easily seen to imply that \(G \cong C_{1,\nu }\)" is the hardest step to formalise, and it is not easy in Lean. Degree sequence does not in general determine a graph up to isomorphism; the implication holds here only because of the specific structure of \(C_{1,\nu }\) and \(C_{2,5}\), and recovering an explicit \(\simeq \)g requires constructing the vertex bijection by hand.

Even degrees everywhere means no "loose ends". Peel cycles off one at a time: removing a cycle subtracts \(2\) from the degree of each vertex it visits, so all degrees stay even and the argument repeats until no edges are left.

"\(E(G) = \bigcup E(C_{i})\) with the \(C_{i}\) edge-disjoint" is rendered as the single \(\exists !\) statement — every edge lies in exactly one of the cycles — which packages covering and disjointness together.

Note this needs no connectivity hypothesis: it is the local content of Euler’s theorem. Connectivity is what additionally lets the cycles be spliced into one tour (Theorem 4.1).

By Corollary 1.1 the odd-degree vertices come in pairs, so there are \(k\) pairs. Pair them up and add \(k\) new edges joining the members of each pair; every vertex of the enlarged graph then has even degree, so Theorem 4.1 gives an Euler tour. Deleting the \(k\) added edges cuts that tour into exactly \(k\) trails, which are edge-disjoint and between them cover every edge of \(G\).

The practical reading: a road network with \(2k\) awkward junctions needs \(k\) separate pen-strokes; one Euler trail is the case \(k = 1\).

A graph that is not 2-connected is either disconnected or has a cut vertex \(v\). Disconnected: no cycle reaches every vertex. Cut vertex: take \(S = {v}\) in Theorem 4.2 — deleting \(v\) leaves at least two components, so \(\omega (G - S) \ge 2 \gt 1 = |S|\), violating the necessary condition.

A Hamilton cycle visits every vertex and returns, which needs two independent routes out of every vertex — exactly 2-connectivity. Necessary but far from sufficient (the Petersen graph is 3-connected and nonhamiltonian).

Stated against this file’s local vertexConnectivity, not the one in Connectivity.lean — see the warning on that definition above.

Every edge crosses between \(X\) and \(Y\), so a cycle alternates sides and uses equally many vertices from each. A Hamilton cycle uses all vertices, forcing \(|X| = |Y|\).

This is why the book’s Herschel graph is nonhamiltonian:

(§4.2, p. 61.) Equivalently, apply Theorem 4.2 with \(S\) the smaller side.

The path analogue of Theorem 4.2. Deleting \(k\) vertices from a path breaks it into at most \(k + 1\) pieces — one more than for a cycle, because a path has two loose ends rather than being closed up. The Hamilton path \(P\) is a spanning subgraph of \(G\), so \(\omega (G - S) \le \omega (P - S) \le |S| + 1\).

The extra \(+1\) is the price of not closing the cycle, making the condition weaker — as it must be, since a Hamilton path is weaker than a Hamilton cycle.

The Hamilton-path counterpart of Theorem 4.5, with thresholds shifted by one. Formalised in counting form, exactly as Theorem 4.5 is — see the note there on why indexing the sorted sequence is avoided.

Note the strict \(d_m \lt m\) here versus \(d_m \le m\) in Theorem 4.5; the hcond filters use \(\lt \) accordingly.

Only part (b) is formalised — part (a) has no separate declaration in this file.

Part (b) from part (a): if \(G \cong G^{c}\) the two sorted degree sequences are identical, so \(d_m \ge d_m'\) holds trivially at every index.

Recall from exercise 1.2.11(b) that self-complementary graphs exist only when \(\nu \equiv 0\) or 1 (mod 4).

This file previously formalised only part (b) (hamiltonian_path_of_self_complementary), even though the book deduces (b) from (a) — so (a) was a hidden prerequisite with no declaration. The triage (log/graphtheory-EXERCISE_TRIAGE.md §A.3) recorded this as a fidelity gap and recommended stating (a). Nothing here is invented: the statement is the book’s own, quoted above.

The two sorted degree sequences are rendered the way chvatal_hamiltonian_path renders its sequence — via a sorting equiv \(\sigma \) on Fin \(\nu \) making the degrees Antitone/Monotone — rather than as raw lists, so the two conditions in this file are stated in the same idiom and can share lemmas.

\(m \le \nu /2\) is written \(2 * m \le \nu \) to avoid \(\mathbb {N}\)-division.

Corollary 4.6 gives a sufficient edge count taking no account of the minimum degree. Erdős’ refinement: when \(\delta \) is known and small relative to \(\nu \), a weaker count suffices — \(C(\nu -\delta , 2) + \delta ^{2}\) rather than \(C(\nu -1, 2) + 1\).

The shape of the bound reflects the extremal configuration: a clique on \(\nu - \delta \) vertices with \(\delta \) low-degree vertices attached, the densest way to be nonhamiltonian while holding the minimum degree at \(\delta \). \(\nu \ge 6\delta \) keeps \(\delta \) genuinely small.

Exercise 1.6.3 already gives a path of length \(\delta \) from the minimum degree alone; Dirac’s sharpening doubles that, at the cost of connectivity and \(\nu \gt 2\delta \).

The bracketed cycle version — 2-connected, \(\nu \ge 2\delta \), cycle of length \(\ge 2\delta \) — is stated but not proved in the chapter. It is what exercise 4.2.10 relies on; see the warning there. It is not stated in this file either.

Such a graph has \(\delta = \Delta = 2k\) and \(\nu = 4k + 1 = 2\delta + 1\), one vertex above the threshold \(\nu \ge 2\delta \) of Dirac’s cycle remark. That remark yields a cycle of length at least \(2\delta = 4k\) — missing at most one vertex — and regularity plus parity then force the cycle to pick up the last vertex too.

! The Lean signature omits the book’s \(k \ge 1\). At \(k = 0\) the statement reads "every \(0\)-regular graph on \(1\) vertex is hamiltonian", which is false in Mathlib: a Hamilton cycle needs length \(\ge 3\), so the one-vertex graph is not IsHamiltonian. The hypothesis \(1 \le k\) must be added.

Hamilton-connectedness demands a spanning path between every pair, forcing many edges. Every vertex must have degree at least \(3\): a degree-\(2\) vertex has both its edges forced into any spanning path through it as an interior vertex, leaving no way to make it an endpoint of a spanning path to a third vertex. Summing \(d(v) \ge 3\) and applying handshaking gives \(2\varepsilon \ge 3\nu \), and a parity refinement pushes this to \(2\varepsilon \ge 3\nu + 1\).

Formalised as \(3\nu + 1 \le 2\varepsilon \) to stay in the natural numbers and avoid the ceiling.

! The Lean signature omits the book’s \(\nu \ge 4\). It is needed: for \(\nu = 3\), \(\top \) on three vertices is Hamilton-connected with \(\varepsilon = 3\), but \(3\nu + 1 = 10 \gt 6 = 2\varepsilon \). So the statement as written is false at \(\nu = 3\) and 4 \(\le \) Fintype.card V must be added.