A transportation network: goods are produced at the sources, consumed at the sinks, and shipped along the arcs, each with a maximum throughput.

! Missing from Mathlib (0 hits for flow/network/capacity). Capacity is carried as a function cap : V \(\to \) V \(\to \) \(\mathbb {N}\), with cap u v = 0 encoding "no arc \(u \to v\)"; this makes \(f^{+}\)/\(f^{-}\) plain Finset.sums. ! It cannot represent parallel arcs, which is a real restriction — lemma 11.4 is about a network in which every arc has unit capacity, and B&M’s digraphs may have several arcs between the same pair.

The structure carries both \(X\), \(Y\) (the source/sink sets of §11.1) and the distinguished \(x\), \(y\) used from §11.2 onward. That is because the book reduces the first to the second: *adjoin two new vertices \(x\) and \(y\); join \(x\) to each vertex in \(X\) by an arc of capacity \(\infty \); join each vertex in \(Y\) to \(y\) by an arc of capacity \(\infty \); designate \(x\) as the source and \(y\) as the sink of \(N'\)* — after which *throughout the next three sections, we shall confine our attention to networks that have a single source \(x\) and a single sink \(y\)*. That reduction is exercise 11.1.4, which is deferred here (it needs an \(\mathbb {N}\infty \)-capacity parallel carrier), so the two are simply both recorded in the structure.

! Structural defect: \(x\), \(y\) are unrelated to \(X\), \(Y\). Nothing in the structure requires N.x \(\in \) N.X, let alone N.X = {N.x}. But val is defined over the set \(X\) while every §11.2–§11.3 result is about cuts separating the single \(x\) from the single \(y\). The two therefore measure different things, and lemma 11.1, theorem 11.1 in both forms, corollary 11.1 and theorem 11.3 are all false as stated.

Counterexample (one network refutes all of them). \(V = {x_{1}, x_{2}, y_{1}}\), \(X = {x_{1}, x_{2}}\), \(Y = {y_{1}}\), N.x = x\(_{1}\), N.y = y\(_{1}\); capacities \(c(x_{1},y_{1}) = c(x_{2},y_{1}) = 1\) and \(0\) elsewhere. Then \(I = \emptyset \), so any \(f\) within capacity is a flow; take \(f(x_{1},y_{1}) = f(x_{2},y_{1}) = 1\). val f = f\(^{+}\)(X) - f\(^{-}\)(X) = 2. \(S = {x_{1}}\) is a cut (\(x_{1} \in S\), \(y_{1} \notin S\)), with \(f^{+}(S) - f^{-}(S) = 1\) and cap S = 1. So lemma 11.1 asserts \(2 = 1\); theorem 11.1 asserts \(2 \le 1\). Max flow value is \(2\), minimum cut capacity is \(1\), so theorem 11.3 asserts \(2 = 1\). Corollary 11.1 fails too: \(f'(x_{1},y_{1}) = 1\), \(f'(x_{2},y_{1}) = 0\) has val f’ = 1 = cap{x\(_{1}\)}, yet \(f'\) is not a maximum flow.

The repair is to add the fields hx : N.X = {N.x} and hy : N.Y = {N.y} to the structure (the book’s standing convention for §§11.2–11.4), or equivalently to add them as hypotheses on the affected theorems. The §11.1 results — exercises 11.1.2 and 11.1.3 — are unaffected and should keep the general \(X\), \(Y\).

The transit points of the network, which neither produce nor consume. The conservation condition (11.2) applies exactly here — what flows in must flow out — and that is what makes val f well defined (exercise 11.1.3).

Finset.univ \{} (X \(\cup \) Y), so \(I\) is a Finset and membership is decidable — needed by IsFlow’s second clause.

The total flow leaving \(S\) — sum over every arc with tail inside \(S\) and head outside. ! This is not the sum of the \(f^{+}(v)\) over \(v \in S\): arcs internal to \(S\) are counted there but not here. Exercise 11.1.2 makes the exact relationship precise, and it is the difference \(f^{+} - f^{-}\) that behaves well.

! Missing from Mathlib. A double Finset.sum over \(S\) and \(S^{c}\), which the capacity-as-a-function carrier makes possible; \(f u v = 0\) for a non-arc contributes nothing.

The total flow entering \(S\). Conservation forces the resultant flow out of every intermediate vertex to vanish, which is what makes the resultant flow out of \(X\) equal the resultant flow into \(Y\) (exercise 11.1.3) and hence val f well defined.

The mirror of fOut with the two sums swapped.

Nothing over-loaded, nothing accumulating. The zero flow’s existence is what makes exists_maxFlow non-vacuous.

The lower bound \(0 \le f(a)\) of (11.1) is free: \(f\) is \(\mathbb {N}\)-valued. Conservation is stated as fIn f {v} = fOut f {v} on singletons, which unfolds to the book’s \(f^{-}(v) = f^{+}(v)\) — note fIn/fOut on a singleton are genuinely the per-vertex quantities, since there are no arcs internal to a singleton.

The net rate at which the commodity travels from producers to consumers. Conservation at the intermediate vertices is what makes the two ways of measuring it agree.

! \(\mathbb {Z}\)-valued, and this is load-bearing. In \(\mathbb {N}\) the truncated subtraction would make exercise 11.1.2 — the identity the whole chapter rests on — false, since individual terms \(f^{+}(v) - f^{-}(v)\) are genuinely negative at vertices absorbing more than they emit. Every \(f^{+} - f^{-}\) in this file is therefore cast to \(\mathbb {Z}\) before subtracting.

A way of severing the network so the source is on one side and the sink on the other. Every unit of flow must cross every cut, which is why cuts bound flows from above (theorem 11.1) — and, more surprisingly, why the best cut exactly matches the best flow (theorem 11.3).

! Missing from Mathlib. Identified with the vertex set \(S\) rather than the arc set \((S, \bar{S})\), since \(S\) determines the arcs and is far easier to quantify over. capOf then computes the arc set’s capacity. Note \(y \notin S\) is the book’s \(y \in \bar{S}\).

The total throughput of the severed arcs — how much traffic could at most cross that divide. Since all the flow must pass through, it bounds val f above.

! Missing from Mathlib. Structurally identical to fOut with cap in place of \(f\), which is exactly why theorem 11.1’s proof is a two-line comparison.

Ship as much as the network allows. Theorem 11.2 characterises these as exactly the flows admitting no incrementing path — the flow-theoretic analogue of Berge’s theorem 5.1 for matchings.

"No flow of larger value" is stated positively as \(\forall \) f’, IsFlow f’ \(\to \) val f’ \(\le \) val f, which is the form every consumer wants.

The cheapest way to sever the network — the bottleneck. Theorem 11.3 says its capacity is exactly the maximum throughput. B&M record the easy half first: If f* is a maximum flow and \(\tilde{K}\) is a minimum cut, we have, as a special case of theorem 11.1, that val f* \(\le \) cap \(\tilde{K}\) (11.8).

As with IsMaxFlow, stated positively.

A route from source to sink along which the flow can still be pushed up. Crucially it may travel against an arc — a reverse arc — provided that arc currently carries positive flow, which can then be cancelled. This is what lets the algorithm undo earlier bad choices, exactly as an augmenting path in matching theory rearranges an existing matching; B&M make the analogy explicit: *the rôle played by incrementing paths in flow theory is analogous to that of augmenting paths in matching theory* (compare theorem 5.1). The book’s example is figure 11.5(a), where \(P = xv_{1}v_{2}v_{3}y\) is \(f\)-incrementing with \(\iota (P) = 2\).

! Missing from Mathlib; an honest, complete inductive family — static, not procedural. nil starts at N.x; fwd extends along an \(f\)-unsaturated arc (f u v < cap u v); back extends against an \(f\)-positive arc (\(0 \lt f v u\)). The index is the current endpoint, so N.IncPath f N.y is exactly an \(f\)-incrementing path.

! This is a directed walk — repeated vertices are allowed — not a path. That is deliberate and is what theorem 11.2’s proof actually uses: the set \(S\) of vertices reachable by \(f\)-unsaturated walks is what the cut is built from, and restricting to paths would complicate the reachability closure for no gain.

The bottleneck along the path. A forward arc has room \(c(a) - f(a)\) left; a reverse arc can give back at most the \(f(a)\) it currently carries. The smallest of these slacks is how much extra can be pushed through in one go.

! Defective: this definition has a sorry body. \(\iota (P)\) is therefore an opaque natural number, not the bottleneck of anything. Consequences: exercise 11.3.1 (revisedFlow_isFlow_and_val) asserts val \(\hat{f}\) = val f + \(\iota \)(P) about two opaque constants and so says nothing, and the forward direction of theorem 11.2 — which needs \(\iota (P) \gt 0\) to get a strictly better flow — has no content to appeal to. This also violates the project convention (.claude/CLAUDE.md): *never sorry in a def*.

The repair is a structural recursion over the IncPath family, carrying the running minimum:

iota nil = \(\top \) (or: recurse with an accumulator seeded at the first arc) iota (fwd P h) = min (iota P) (cap u v - f u v) iota (back P h) = min (iota P) (f v u)

The only wrinkle is nil, which has no arcs and so no minimum; either return a sentinel and prove 0 < iota P for non-nil paths, or index the recursion by a running minimum passed in. The second is cleaner and avoids \(\mathbb {N}\infty \).

Push \(\iota (P)\) more along every forward arc of the path and take \(\iota (P)\) back off every reverse arc. Conservation survives because at each interior vertex the increase in and the increase out match; and the value rises by exactly \(\iota (P)\) (exercise 11.3.1). This is the engine of the labelling method: repeatedly find an incrementing path and revise, until none exists — at which point theorem 11.2 certifies maximality.

! Defective: this definition has a sorry body. \(\hat{f}\) is an opaque function, so exercise 11.3.1 — the only statement about it — is vacuous, and theorem 11.2’s forward direction has nothing to revise with. Same convention violation as iota.

The repair is a structural recursion over IncPath mirroring iota’s, adjusting one arc per constructor:

revisedFlow nil = f revisedFlow (fwd P _) = Function.update\(_{2}\) (revisedFlow P) u v (f u v + iota P) revisedFlow (back P _)= Function.update\(_{2}\) (revisedFlow P) v u (f v u - iota P)

! Note iota P must be the bottleneck of the whole path, not of the prefix, or the capacity constraint fails on early arcs — so iota should be computed once and threaded, rather than recomputed at each step. That coupling is the reason both definitions were deferred together, and it is why repairing iota first is the right order.

Corollary 11.5 relates it to edge-disjoint paths: \(G\) is \(k\)-edge-connected exactly when any two distinct vertices are joined by \(k\) edge-disjoint paths — the global connectivity number turned into a local path count.

A minimal local copy; the real one lives in TCSlib.GraphTheory.Connectivity, deliberately not imported so this file stands alone. ! sInf \(\emptyset \) = 0, so a graph with no edge cut (a one-vertex graph) gets \(\kappa ' = 0\) — a boundary case that will bite corollary 11.5 exactly as it bit chapter 10’s associatedDigraph_isKArcConnected_iff.

Corollary 11.7 relates it to internally-disjoint paths: \(G\) with \(\nu \ge k + 1\) is \(k\)-connected exactly when any two distinct vertices are joined by \(k\) internally-disjoint paths. This is the form of Menger’s theorem §3.2 announced without proof.

A minimal local copy, as for edgeConnectivity. The \(\nu - 1\) branch is the book’s convention for graphs with no vertex cut (complete graphs). ! Both sInf conventions bite at the boundaries — see the outline.

The paths share only their endpoints. This is the notion in which Menger’s vertex theorem 11.7 and corollary 11.7 are phrased, and — via the vertex splitting of theorem 11.6 — it is what arc-disjointness in the split digraph corresponds to.

A minimal local copy (the repo’s is TwoConnected.lean:58), stated for a pair of walks. ! Menger’s theorem needs internal disjointness of a whole family; extending this pairwise predicate to families is part of what maxInternallyDisjointPaths must do, and is one reason that count was stubbed.

For a unit-capacity network this equals the value of a maximum flow: each path carries one unit, and arc-disjointness is exactly the capacity constraint.

! sorry body. Repair: sSup over \(k\) such that there are \(k\) directed \((x,y)\)-paths in the underlying digraph (arcs = pairs with 0 < cap u v) that are pairwise arc-disjoint. Needs a directed-path notion; see the section note.

For a unit-capacity network this equals the value of a maximum flow: each path carries one unit, and arc-disjointness is exactly the capacity constraint.

! sorry body. Repair: sSup over \(k\) such that there are \(k\) directed \((x,y)\)-paths in the underlying digraph (arcs = pairs with 0 < cap u v) that are pairwise arc-disjoint. Needs a directed-path notion; see the section note.

The left-hand side of Menger’s arc theorem 11.4: how many routes from \(x\) to \(y\) can run simultaneously without any two sharing an arc.

! sorry body. Repair: sSup over \(k\) admitting \(k\) pairwise arc-disjoint directed \((x,y)\)-paths. Needs a directed-path notion (Digraph.IsDirectedPath in the ch-10 file) and an arc-list, which is arcsOf there — itself sorry-bodied. Of the twelve, this is the one with the deepest dependency.

The left-hand side of Menger’s arc theorem 11.4: how many routes from \(x\) to \(y\) can run simultaneously without any two sharing an arc.

! sorry body. Repair: sSup over \(k\) admitting \(k\) pairwise arc-disjoint directed \((x,y)\)-paths. Needs a directed-path notion (Digraph.IsDirectedPath in the ch-10 file) and an arc-list, which is arcsOf there — itself sorry-bodied. Of the twelve, this is the one with the deepest dependency.

The right-hand side of Menger’s arc theorem 11.4: how few arcs must be cut to sever \(x\) from \(y\) entirely.

! sorry body. Repair: sInf {k | \(\exists \) Z : Finset (V \(\times \) V), Z.card = k \(\land \) \(\lnot \) Relation.ReflTransGen (fun u v => D.Adj u v \(\land \) (u,v) \(\notin \) Z) x y}.

— reachability suffices.

The left-hand side of Menger’s vertex theorem 11.6 — routes sharing no intermediate vertex, so destroying any one interior station leaves the others intact.

! sorry body. Repair: as for the arc version but with internal-vertex disjointness, which needs only the paths’ vertex lists (Quiver.Path.vertices), not arcsOf — so it is easier than maxArcDisjointDirectedPaths.

The left-hand side of Menger’s edge theorem 11.5, the undirected counterpart of theorem 11.4.

! sorry body — definable today. Repair: sSup {k | \(\exists \) ps : Fin k \(\to \) G.Walk x y, (\(\forall \) i, (ps i).IsPath) \(\land \) \(\forall \) i j, i \(\ne \) j \(\to \) List.Disjoint (ps i).edges (ps j).edges}. Every ingredient (Walk, IsPath, Walk.edges, List.Disjoint) is already imported.

The left-hand side of Menger’s edge theorem 11.5, the undirected counterpart of theorem 11.4.

! sorry body — definable today. Repair: sSup {k | \(\exists \) ps : Fin k \(\to \) G.Walk x y, (\(\forall \) i, (ps i).IsPath) \(\land \) \(\forall \) i j, i \(\ne \) j \(\to \) List.Disjoint (ps i).edges (ps j).edges}. Every ingredient (Walk, IsPath, Walk.edges, List.Disjoint) is already imported.

The right-hand side of Menger’s edge theorem 11.5.

! sorry body — definable today. Repair: sInf {k | \(\exists \) F : Finset (Sym2 V), F.card = k \(\land \) \(\lnot \) (G.deleteEdges ↑F).Reachable x y}. deleteEdges and Reachable are already imported.

The left-hand side of Menger’s vertex theorem 11.7 — the form quoted back in §3.2, where it generalises Whitney’s theorem 3.2 from \(k = 2\) to all \(k\).

! sorry body — definable today. Repair: as maxEdgeDisjointPaths but with \(\forall \) i j, i \(\ne \) j \(\to \) InternallyDisjoint (ps i) (ps j), using the local pairwise InternallyDisjoint above.

The "fan" or set-to-set form of Menger’s theorem, where the endpoints are not fixed but merely constrained to lie in prescribed sets. This is the form exercise 11.4.4 (Dirac) actually consumes.

! sorry body — definable today. Repair: sSup over \(k\) admitting \(k\) paths, each with one end in \(S\) and one in \(T\), pairwise vertex-disjoint (not merely internally disjoint — the endpoints must differ too, which is why this is not a special case of maxInternallyDisjointPaths). A \(\Sigma \)-typed family Fin k \(\to \) \(\Sigma \) u \(\in \) S, \(\Sigma \) v \(\in \) T, G.Walk u v handles the varying endpoints.

The "fan" or set-to-set form of Menger’s theorem, where the endpoints are not fixed but merely constrained to lie in prescribed sets. This is the form exercise 11.4.4 (Dirac) actually consumes.

! sorry body — definable today. Repair: sSup over \(k\) admitting \(k\) paths, each with one end in \(S\) and one in \(T\), pairwise vertex-disjoint (not merely internally disjoint — the endpoints must differ too, which is why this is not a special case of maxInternallyDisjointPaths). A \(\Sigma \)-typed family Fin k \(\to \) \(\Sigma \) u \(\in \) S, \(\Sigma \) v \(\in \) T, G.Walk u v handles the varying endpoints.

Make every street two-way. B&M call it a simple trick: it is how theorems 11.5 and 11.7 are deduced from their directed counterparts 11.4 and 11.6, since paths in \(G\) correspond exactly to directed paths in \(D(G)\).

One line — G.Adj is already symmetric, so it is the arc relation. A local copy of chapter 10’s SimpleGraph.associatedDigraph; the path correspondence that makes the trick work is that file’s associatedDigraph_pathEquiv, which is itself sorry-bodied there.

Each vertex becomes a tiny one-way corridor \(v' \to v''\), so *passing through* \(v\) now costs an arc. This converts vertex-destruction into arc-destruction, letting the vertex form of Menger’s theorem be read off from the arc form: *two directed \((x,y)\)-paths in \(D'\) are arc-disjoint if and only if the corresponding paths in \(D\) are internally-disjoint.*

! Missing from Mathlib. Carrier \(V \oplus V\), with inl v = v’ and inr v = v”; internal arcs are inl u \(\to \) inr v when \(u = v\), and original arcs become inr u \(\to \) inl v.

! Simplified: it does not special-case \(x\) and \(y\). The book splits only \(V \ {x, y}\), leaving the endpoints intact; this splits every vertex. The consequence is that \(x\) and \(y\) also acquire internal arcs, so a destroying set in \(D'\) could cut \(x\)’s or \(y\)’s own corridor — which corresponds to deleting \(x\) or \(y\) themselves, something the book’s vertex-destruction forbids. Statements about splitDigraph therefore address Sum.inr x and Sum.inl y (the far ends of those corridors), which sidesteps the issue for exercise 11.4.1; but the simplification should be checked before it is relied on elsewhere.

for supplies \(\sigma \) and demands dem (B&M’s \(\partial \)). ! MISSING. Honest def.

Nobody ships more than they can produce, and everybody receives at least what they ordered. Gale’s theorem 11.8 characterises existence: for every \(S\), the capacity out of \(S\) must cover the net demand of \(\bar{S}\).

! Missing from Mathlib. dem is B&M’s \(\partial \). Both conditions are cast to \(\mathbb {Z}\) before subtracting, for the reason recorded under val. Supplies and demands are \(V \to \mathbb {N}\) total functions, with the conditions quantified only over \(X\) and \(Y\), so their values elsewhere are irrelevant.

Can two prescribed lists of degrees occur as the two sides of a bipartite graph? The book’s \(p = (3,2,2,2,1)\), \(q = (3,3,2,1,1)\) is realisable (figure 11.12), whereas \(p = q = (5,4,4,2,1)\) is not (exercise 11.5.2) even though the sums agree.

! Missing from Mathlib (0 hits for Gale–Ryser). Carried as a \((0,1)\)-matrix B : Fin m \(\to \) Fin n \(\to \) Bool rather than a bipartite SimpleGraph, following the book’s own closing remark: *With each simple bipartite graph \(G\) …we can associate an \(m \times n\) matrix \(B\) in which \(b_ij = 1\) or \(0\), depending on whether \(x_{i}y_{j}\) is an edge of \(G\) or not. Conversely, every \(m \times n\) \((0,1)\)-matrix corresponds in this way to a simple bipartite graph.* The two are equivalent and the matrix avoids constructing a graph on Fin m \(\oplus \) Fin n with a bipartition proof. Due to Ryser (1957).

Make every edge one-way so each vertex ends up receiving exactly \(m\) arrows, or exactly \(n\). Since \(G\) is \((m+n)\)-regular, indegree \(m\) forces outdegree \(n\) and conversely, so an orientation splits the vertices into two classes. Exercise 11.5.5(a) characterises orientability by a cut condition, and (b) shows the classes can always be rebalanced one step towards each other.

! Missing from Mathlib (0 hits for "orientable"). The orientation is spelled out inline as a Digraph D with three clauses — \(D \subseteq G\), \(D\) never two-way, \(D\) covers every edge — rather than reusing chapter 10’s IsOrientationOf, which this file does not import. The fourth clause is the indegree condition. Note the \((m+n)\)-regularity is not part of this definition; it appears as a hypothesis on the theorems that use it.

The size of the undirected edge cut at \(S\) — how many edges would have to be severed to separate \(S\) from the rest. In exercise 11.5.5(a) it is the capacity available to carry the imbalance the prescribed indegrees force across \(S\)’s boundary.

A double sum of indicators rather than a Finset.card, matching the shape of fOut/capOf so the three compare directly. Since G.Adj is symmetric and the sum runs over \(S \times S^{c}\), each crossing edge is counted once.