Chapter 26 - Maximum Flow

Chapter 26 opens the maximum-flow part of the CLRS graph track. The current partial development builds a finite capacity-function model, proves concrete Ford--Fulkerson augmentation and the full Max-Flow Min-Cut equivalence, and exposes infrastructure for the later algorithms.

Sections

• 26.1 Flow networks. Main declarations: CLRS.Chapter26.FlowNetwork, CLRS.Chapter26.Flow, CLRS.Chapter26.Flow.value, CLRS.Chapter26.Flow.netFlow_eq_value, CLRS.Chapter26.Flow.residualCapacity, CLRS.Chapter26.Flow.residualEdge, CLRS.Chapter26.Flow.augmentingPathReachable, CLRS.Chapter26.Flow.maximal_of_noAugmentingPath, and CLRS.Chapter26.Flow.exists_cut_value_eq_of_noAugmentingPath.

• 26.2 Ford-Fulkerson augmentation. Main declarations: CLRS.Chapter26.Flow.ResidualPath, CLRS.Chapter26.Flow.AugmentingPath, CLRS.Chapter26.Flow.AugmentingPath.bottleneck, CLRS.Chapter26.Flow.augmentBy, CLRS.Chapter26.Flow.augment, CLRS.Chapter26.Flow.augmentBy_value, CLRS.Chapter26.Flow.augment_value, CLRS.Chapter26.Flow.value_lt_augment, CLRS.Chapter26.Flow.hasAugmentingPath_iff_nonempty_augmentingPath, and CLRS.Chapter26.Flow.not_maximal_of_hasAugmentingPath.

• 26.2 Edmonds-Karp analysis. Main declarations: CLRS.Chapter26.ResidualPathLength, CLRS.Chapter26.IsShortestDist, CLRS.Chapter26.isShortestDist_self, CLRS.Chapter26.IsShortestDist.unique, CLRS.Chapter26.isShortestDist_triangle, CLRS.Chapter26.IsShortestDist.exists_predecessor, CLRS.Chapter26.ShortestAugmentingPath, CLRS.Chapter26.ShortestAugmentingPath.shortest_prefix, CLRS.Chapter26.ShortestAugmentingPath.exists_shortestDist_le_augment, and CLRS.Chapter26.shortest_path_nondec (Lemma 26.7).

• 26.3 Maximum bipartite matching. Main declarations: CLRS.Chapter26.BipartiteGraph, CLRS.Chapter26.Matching, CLRS.Chapter26.toFlowNetwork, CLRS.Chapter26.matchingToFlow, CLRS.Chapter26.matchingToFlow_value, CLRS.Chapter26.matchingOfIntegralFlow, CLRS.Chapter26.matchingOfIntegralFlow_size, and CLRS.Chapter26.maxMatching_eq_maxFlow_value (Theorem 26.12).

• 26.4 Push-relabel algorithms. Main declarations: CLRS.Chapter26.Preflow, CLRS.Chapter26.Preflow.excess, CLRS.Chapter26.Preflow.isOverflowing, CLRS.Chapter26.IsValidHeight, CLRS.Chapter26.admissibleEdge, CLRS.Chapter26.Preflow.pushBy, CLRS.Chapter26.Preflow.push, CLRS.Chapter26.relabel, CLRS.Chapter26.height_le_of_overflowing (Lemma 26.15), and CLRS.Chapter26.maximal_of_no_overflow.

• Theorem 26.6, Max-Flow Min-Cut. Main declarations: CLRS.Chapter26.Flow.eq_cutCapacity_implies_maximal, CLRS.Chapter26.Flow.maximal_iff_noAugmentingPath, and CLRS.Chapter26.Flow.maximal_iff_exists_cut_value_eq.

Current Shape

Section 26.1 defines a FlowNetwork as a capacity function c : V → V → ℝ together with a distinguished source s and sink t. A feasible flow Flow satisfies capacity constraint, skew symmetry, and flow conservation. The section proves Lemma 26.5 (net flow across any cut equals flow value) and the generic Ford-Fulkerson correctness theorem: if there is no augmenting path in the residual network, the flow is maximal.

The Ford-Fulkerson augmentation module packages a concrete simple residual source-to-sink path, proves that its bottleneck is positive, constructs the resulting feasible augmented flow, and proves both its exact and strict value increase. It also converts residual source-to-sink reachability to this concrete simple-path representation and uses augmentation to prove that any flow with an augmenting path is not maximal.

The Edmonds-Karp module defines residual path lengths and shortest residual distances. It proves predecessor and shortest-prefix facts, characterizes the new residual edges introduced by augmentation, and combines those bridges into the monotonic residual-distance theorem of Lemma 26.7. The companion submodules assemble the explicit shortest augmenting path from residual reachability, run the Edmonds-Karp loop to an integral maximal flow (edmondsKarp_maximal), prove the critical-edge counting argument that bounds the number of augmentations by O(VE²) (critical_count_bound, augmentation_count_bound), and supply an executable breadth-first search (residualBFS) whose parent chain yields the shortest augmenting path (bfs_shortestAugmenting).

Section 26.3 defines bipartite graphs, matchings, and the unit-capacity reduction. It constructs the feasible flow induced by every matching (matchingToFlow) with value equal to its size, recovers a matching of size v from every integral flow of value v (matchingOfIntegralFlow), and iterates shortest-free augmentation from the zero flow to obtain an integral maximum flow. These pieces combine into CLRS Theorem 26.12 (maxMatching_eq_maxFlow_value): the maximum matching size equals the maximum flow value.

The companion file Section_26_6_MaxFlow_MinCut proves the full Max-Flow Min-Cut Theorem: maximality is equivalent both to the absence of a residual source-to-sink path and to equality with the capacity of some cut.

Section 26.4 (push-relabel) formalizes the preflow-push model: a Preflow relaxes conservation to nonnegative excess off the source, a valid height function (IsValidHeight) bounds residual-edge height drops by one, and the Preflow.pushBy and relabel operations preserve both invariants. The overflowing-vertex source-reachability lemma and the 2|V| - 1 height bound (height_le_of_overflowing, Lemma 26.15) supply the termination foundation, and maximal_of_no_overflow combines a valid height function with zero internal excess to certify maximality via the max-flow min-cut theorem.

Deferred Work

Section 26.5 (relabel-to-front) and the fine-grained saturating/nonsaturating push count (O(V²E)/O(V³)) are deferred outside the current selected milestone.