Both directions are stated contrapositively relative to the book’s phrasing: the Lean \(\leftrightarrow \) has "no augmenting path" on the right, so the book’s first paragraph proves (\(\Rightarrow \)) by contraposition and its second proves (\(\Leftarrow \)) by contraposition.

Augmenting paths are simultaneously the certificate of non-maximality and the means of improvement — which is what makes the Hungarian method of §5.4 work.

Hall’s condition: no set of vertices on the \(X\) side may collectively have too few neighbours. Colloquially — no group of \(k\) workers may be jointly qualified for fewer than \(k\) jobs.

\(N(S)\) is written \(\bigcup \) v \(\in \) S, G.neighborSet v, and the inequality is stated as S.ncard \(\le \) (\(\bigcup \) …).ncard — the book’s \(|N(S)| \ge |S|\) with sides swapped.

Two applications of double counting, then Hall. The book’s colourful restatement, from which the name comes (§5.2, p. 81):

The edges of a matching are pairwise disjoint and the covering must contain an endpoint of each; since no two matching edges share an endpoint, the chosen endpoints are distinct, so \(K\) has at least \(|M|\) elements.

The book continues:

which is König’s Theorem 5.3.

The standard "weak duality certifies optimality" argument: exhibiting a matching and a covering of the same size proves both optimal at once. It is exactly how Theorem 5.3 is proved.

The prototypical min-max theorem of combinatorics — maximum packing equals minimum cover. Closely related to Hall’s theorem: exercise 5.2.7 asks to derive Hall from König, and its matrix form is exercise 5.2.5.

Note the Lean statement takes both extremal objects as hypotheses (hM, hK) and concludes their sizes agree, rather than constructing \(\tilde{K}\) as the book does.

The obstruction to a perfect matching is a set \(S\) whose removal leaves more odd pieces than \(S\) has vertices — each odd piece must "export" a vertex to be matched into \(S\).

A double count per odd component, then Tutte. The parity step is the crux: \(m_{i} = 3\nu (G_{i}) - 2\varepsilon (G_{i})\) is odd because \(\nu (G_{i})\) is odd, and bridgelessness then upgrades \(m_{i} \ge 1\) to \(m_{i} \ge 3\).

! The book’s \(\tfrac {1}{3} \sum m_{i} \le \tfrac {1}{3} \sum _{v \in S} d(v)\) is over \(\mathbb {Q}\). In \(\mathbb {N}\) this should be cleared to \(3n \le \sum m_{i} \le 3|S|\) and divided only at the end, or done in \(\mathbb {Z}\).

Weak duality certifying optimality again: \(\sum _v l(v)\) bounds every perfect matching from above, and one attaining the bound must be best. This is the foundation of the Kuhn–Munkres algorithm, which alternates the Hungarian method inside \(G_l\) with label adjustments that grow \(G_l\).

The conclusion transports \(M\) along Hom.ofLE from equalitySubgraph w G l up to \(G\), since the two live over different graphs.

The \(k\)-cube is \(k\)-regular and bipartite (sides given by the parity of the number of \(1\)s), so for \(k \ge 2\) Corollary 5.2 applies.

A perfect matching of \(K_{2n}\) partitions \(2n\) labelled objects into \(n\) unordered pairs. Lining them up gives \((2n)!\) arrangements; each matching arises from \(2^n \cdot n!\) of them (swap within each pair, permute the pairs). So the count is \((2n)! / (2^n \cdot n!)\), the double factorial \((2n-1)!! = 1 \cdot 3 \cdot 5 \cdots (2n-1)\).

! The Lean statement uses natural-number division. It happens to be exact here, but the proof cannot manipulate it as division — it must establish Nat.card … (2 ^ n n !) = (2 * n)! and then divide, or the Nat.div will obstruct every rewrite.

Every vertex of \(X\) may be matched to any vertex of \(Y\), so a perfect matching is exactly a bijection \(X \to Y\). There are \(n!\) of those.

This is why the optimal assignment problem of §5.5 has \(n!\) candidate solutions and brute force is hopeless — the book makes exactly that point on p. 94.

Suppose a tree had two perfect matchings \(M \ne M'\). Every vertex meets at most one edge of each, so every vertex of \(M \Delta M'\) has degree one or two and its components are alternating paths and even cycles. Both matchings being perfect, no vertex is an endpoint of such a path, so only cycles occur — impossible in an acyclic graph. Hence \(M \Delta M' = \emptyset \).

Label both sides by ZMod n; for each \(i\), let \(H_{i}\) join \(x_a\) to \(y_{a+i}\) for every \(a\). Each \(H_{i}\) is a 1-factor, distinct \(i\) give edge-disjoint matchings, and every edge \(x_a y_b\) occurs in exactly the one with \(i = b - a\).

In chapter 6’s language: \(K_{n,n}\) has chromatic index \(n\), its minimum possible value — the round-robin schedule for \(n\) workers and \(n\) jobs.

The classical round-robin schedule. Fix one vertex at the centre and arrange the other \(2n - 1\) in a circle. In round \(i\), match the centre with circle vertex \(i\) and pair the remaining circle vertices symmetrically about the line through it. Rotating gives \(2n - 1\) rounds, each a perfect matching, together using every edge exactly once.

So \(2n\) players can be scheduled in \(2n - 1\) rounds with every pair meeting once. This fails for odd order, where no perfect matching exists at all.

\(\delta \ge \nu /2 + 1\) is one better than Dirac’s threshold, so Theorem 4.3 gives a Hamilton cycle \(C\). With \(\nu \) even, \(C\) is an even cycle whose edges split alternately into two perfect matchings. Removing \(C\)’s edges drops every degree by \(2\), leaving enough for a second Hamilton cycle; combining the 2-factor \(C\) with a 1-factor from the second gives degree \(3\) everywhere.

\(\delta \ge \nu /2 + 1\) is formalised as \(\nu + 2 \le 2\delta \) to stay in the natural numbers.

A connected 2-factor is precisely a Hamilton cycle — a spanning connected 2-regular subgraph must be one cycle through every vertex. So this asks for a decomposition of \(K_{2n+1}\)’s edges into Hamilton cycles.

The count works: \(K_{2n+1}\) has \(n(2n+1)\) edges and each Hamilton cycle uses \(2n + 1\), so exactly \(n\) cycles are needed.

The odd-order companion to 5.1.5(a)(i): odd complete graphs decompose into Hamilton cycles, even ones into perfect matchings.

Hall’s Theorem 5.2 gives a matching saturating \(X\) from the condition on subsets of \(X\) alone. Demanding it for all subsets of \(V\) is symmetric in \(X\) and \(Y\), so it yields matchings saturating each side; together these force \(|X| = |Y|\) and a perfect matching.

! hcov : X \(\cup \) Y = Set.univ is required and has no counterpart in the book’s wording, which takes "bipartition" to cover all vertices by definition. Mathlib’s IsBipartiteWith does not, so without hcov the bipartition could miss vertices that no matching could ever saturate.

Corollary 5.2 gives a perfect matching \(M\). Deleting its edges lowers every degree by one, leaving a \((k-1)\)-regular bipartite graph; iterate \(k\) times.

In chapter 6’s language this is \(\chi '(G) = \Delta (G)\) for bipartite graphs — König’s edge-colouring theorem. In scheduling terms, a balanced workload always splits into \(k\) conflict-free rounds.

Every degree is even, so Theorem 4.1 gives each component an Euler tour. Traverse it and orient each edge in the direction of travel; every vertex then has in-degree \(k\) and out-degree \(k\), since the tour enters and leaves it \(k\) times. Build the bipartite "tail/head" double cover, joining tail \(u\) to head \(v\) for each oriented edge \(u \to v\). That graph is \(k\)-regular, hence 1-factorable by part (a); translating each perfect matching back gives a spanning subgraph with one in-edge and one out-edge per vertex — a 2-factor.

König’s Theorem 5.3 in matrix dress. A vertex per row and per column, joining row \(i\) to column \(j\) when A i j = true. Lines covering all the \(1\)s are a vertex covering; \(1\)s no two sharing a line are a matching.

The IsLeast/IsGreatest hypotheses supply the two optima as given, so this statement only has to equate them. "No two in the same line" is rendered as the pair of InjOn conditions on Prod.fst and Prod.snd.

Hall’s theorem says a matching saturating \(X\) exists exactly when \(|S| - |N(S)| \le 0\) for all \(S \subseteq X\). The defect formula quantifies failure: the largest \(|S| - |N(S)|\), the deficiency, is exactly how many vertices of \(X\) a maximum matching must leave unsaturated. Hall is the zero-deficiency case.

Formalised additively as |M| + deficiency = |X| to avoid \(\mathbb {N}\) subtraction on the outside.

! But the inner S.ncard - (\(\bigcup \) …).ncard is still natural subtraction, so it truncates to \(0\) exactly when Hall’s condition holds at \(S\) — which is what makes the \(\bigsqcup \) compute the book’s max{…} correctly only because the book’s max is also effectively taken against \(0\) (via \(S = \emptyset \)). This is a happy accident rather than a faithful rendering, and is worth re-checking when the proof is attempted.

By the defect formula, a maximum matching smaller than \(k\) forces some \(S \subseteq X\) with large \(|S| - |N(S)|\). Every edge meeting \(S\) then ends inside the small set \(N(S)\), and simplicity caps the total edge count at \((k-1)n\) — contradiction.

Equivalently, via König: a covering of size \(\lt k\) caps \(\varepsilon \) at \((k-1)n\), since each covering vertex has degree at most \(n\).

Sum every entry two ways. By rows: \(1\) each, so \(m\) in total. By columns: \(1\) each, so \(n\). Hence \(m = n\).

! Restated, not transcribed. Mathlib’s doublyStochastic is square *by type*, so the literal statement would be vacuous. This version takes a genuinely rectangular Matrix m n \(\mathbb {R}\) with the two summation hypotheses given explicitly, which is what the exercise actually asks.

Note the non-negativity hypothesis is not needed for this part and is omitted.

Left and right cosets each partition \(H\) into \(n = [H : K]\) blocks of size \(|K|\). The claim: one list of \(n\) elements represents both partitions simultaneously.

Hall again — put left cosets on one side, right cosets on the other, joining aK to Kb when they intersect. All cosets having size \(|K|\) makes this graph regular, so Corollary 5.2 gives a perfect matching; choosing an element from each matched intersection is the common transversal.

! The Lean rendering states the two conclusions as Function.Bijective of the maps \(i \mapsto h_{i} \textbullet {} K\) and \(i \mapsto op h_{i} \textbullet {} K\) into Set H. The note in the file flags this shape as provisional, and it is worth scrutiny: bijectivity onto what codomain is left implicit (it is Set H, not the set of cosets), so as written the maps are into a far larger type than intended and the statement may be stronger — or simply wrong — relative to the exercise. Recheck before proving.

Petersen’s argument at general \(k\). For \(S \subset V\) with odd components \(G_{i}\) of \(G - S\) and \(m_{i}\) the edges from \(G_{i}\) to \(S\): regularity gives \(m_{i} = k\nu (G_{i}) - 2\varepsilon (G_{i})\), of the same parity as \(k\nu (G_{i})\). Those edges form an edge cut, so \((k-1)\)-edge-connectivity gives \(m_{i} \ge k - 1\), and parity upgrades that to \(m_{i} \ge k\) where needed. Summing, \(k \cdot o(G - S) \le \sum m_{i} \le \sum _{v \in S} d(v) = k|S|\).

Corollary 5.4 is the case \(k = 3\): a bridgeless cubic graph is 2-edge-connected.

Tutte’s condition quantifies over all \(S\), but for trees the singletons already decide it.

(\(\Rightarrow \)) The partner of \(v\) lies in one component of \(G - v\), and a parity count shows exactly one component is odd.

(\(\Leftarrow \)) \(o(G - v) = 1\) for every \(v\) is Tutte’s condition at singletons, and acyclicity makes that enough: build greedily from the leaves, each leaf forced to match its unique neighbour.

Combined with exercise 5.1.2, a tree’s perfect matching — when it exists — is unique and locally detectable.

Tutte says a perfect matching exists exactly when \(o(G - S) - |S| \le 0\) for all \(S\). Berge’s formula quantifies failure: the maximum, the deficiency \(d\), is exactly how many vertices a maximum matching leaves unsaturated; the remaining \(\nu - d\) pair up.

\(d = 0\) recovers Theorem 5.4. The general-graph analogue of the König–Ore defect formula (5.2.6(a)).

Formalised additively as \(2|M| + d = \nu \) to avoid \(\mathbb {N}\) subtraction on the outside.

! Same caveat as konig_ore_defect: the inner oddComponents.ncard - S.ncard is still natural subtraction and truncates at \(0\). Here that is actually correct, since \(S = \emptyset \) always contributes \(o(G) - 0 \ge 0\) and the book’s max is over a set containing a non-negative value — but it should be re-verified rather than assumed.

An edge-count sufficient condition, in the spirit of Corollary 4.6 for hamiltonicity. The threshold is the edge count of the densest simple graph on \(\nu \) vertices with minimum degree \(\delta \) that still violates Tutte’s condition: a \(\delta \)-set \(S\) whose removal leaves too many odd components, plus as many edges as can be packed around it. Exceeding it leaves no room to violate Tutte.

Part (a) — "characterise the maximal simple graphs which have no perfect matching" — has no propositional content and is dropped; the book’s answer is recorded in the dropped-items section at the end of this file.