All missions

Motivation

In a communication or transportation network, a planner often needs not one maximal flow value but all of them: the largest amount that can be sent between every pair of locations. For an undirected network with $n$ nodes there are $n(n-1)/2$ such values. In 1961, R. E. Gomory and T. C. Hu (Multi-terminal network flows, J. SIAM 9 (1961)) answered two questions about them. Which tables of numbers can occur as the all-pairs maximal flow values of some network? And how many maximal flow computations are needed to find them all? Mayeda (1960) and Chien (1960) studied the same questions at about the same time.

Ford and Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) gives the theory in its fourth chapter, "Multi-Terminal Maximal Flows", following Gomory and Hu. This mission formalizes the first half of that chapter: the cycle criterion for maximal spanning subtrees (§1), the characterization of flow functions and their realization by trees (§2), and the condensation lemma behind the Gomory–Hu procedure (§3).

Setting

An undirected network $G$ has a finite set $N$ of nodes and a set of undirected arcs. An arc joins two distinct nodes, and at most one arc joins any two nodes. Each arc $\{x, y\}$ carries a nonnegative real capacity $c(x, y) = c(y, x)$.

A flow of value $w$ from $s$ to $t$ assigns to each ordered pair a number $f(x, y) \ge 0$, the flow from $x$ to $y$. It vanishes unless $\{x, y\}$ is an arc. On each arc it satisfies $f(x, y) \le c(x, y)$, $f(y, x) \le c(x, y)$ and $f(x, y)\,f(y, x) = 0$, so flow moves in only one direction. The net flow out of a node, $f(x, N) - f(N, x)$, is $w$ at $s$, $-w$ at $t$, and $0$ at every other node. The maximal flow value from $x$ to $y$ is the largest value of a flow from $x$ to $y$. The book calls the function $v(x, y)$ giving this value for every pair of distinct nodes the flow function of $G$. It is symmetric, and $v(x, x)$ is left undefined.

A symmetric function $v \ge 0$ on pairs of distinct nodes is realizable if some undirected network on $N$ has flow function $v$. It is realizable by a tree if the arcs of such a network form a tree on $N$, that is, a connected graph without cycles.

For a set $X$ of nodes with complement $\bar X = N - X$, the cut capacity $c(X, \bar X)$ is the total capacity of the arcs joining $X$ to $\bar X$. $(X, \bar X)$ is a minimal cut separating $s$ and $t$ if $s \in X$, $t \in \bar X$, and no other such node set has a smaller cut capacity. The condensed network shrinks all of $\bar X$ to a single node. Arcs between nodes of $X$ (the ordinary nodes) are kept. The arcs from an ordinary node $x$ to $\bar X$ become one arc whose capacity is their sum.

Given a connected graph $G$ with real arc lengths $a(x, y)$, a spanning subtree is a tree $T$ obtained from $G$ by deleting arcs. Arcs of $T$ are in-tree and the rest are out-of-tree. $T$ is maximal if no spanning subtree of $G$ has a larger total length.

Formalization targets

Goal: Chapter IV, Theorem 2.1 (p. 8)

For a nonempty finite node set $N$ and a symmetric $v \ge 0$ on pairs of distinct nodes, $v$ is realizable if and only if, for all pairwise distinct $x, y, z$,

$$v(x, y) \ge \min\,[v(x, z), v(z, y)]. \tag{2.1}$$

Moreover, if $v$ is realizable, it is realizable by a tree.

Milestones

1. Theorem 1.1 (p. 5). A spanning subtree $T$ is maximal if and only if, for each out-of-tree arc $\{x_1, x_k\}$ with in-tree chain $x_1, x_2, \dots, x_k$,

$$a(x_1, x_k) \le \min\,[a(x_1, x_2), \dots, a(x_{k-1}, x_k)]. \tag{1.1}$$

2. Lemma 2.1 (p. 6). Every flow function satisfies (2.1).
3. Lemma 2.2 (p. 8). Every symmetric $v \ge 0$ satisfying (2.1) is the flow function of some undirected network.
4. Lemma 3.1 (p. 11). Let $(X, \bar X)$ be an $s, t$ minimal cut, and let $x, y$ be two distinct nodes of $X$. The maximal flow value $v'(x, y)$ in the network condensed at $\bar X$ equals the maximal flow value $v(x, y)$ in the original network.

Significance

Theorem 2.1 says that the all-pairs maximal flow values of an undirected network take a very restricted form. Every network is flow-equivalent to a tree on the same nodes. At most $n - 1$ distinct values occur. Every value is a minimum of values along a path. The Gomory–Hu tree, with its $n - 1$ maximal flow computations instead of $n(n-1)/2$, rests on this structure, and Lemma 3.1 is what makes that procedure correct: each later flow problem can be solved on a smaller, condensed network without changing the answer. Gomory–Hu trees are used in network reliability, in the separation of odd-cut inequalities for matching polytopes (Padberg and Rao, 1982), and in graph clustering. Theorem 1.1 is the cycle-optimality criterion for maximum-weight spanning trees. It underlies the correctness of Kruskal's algorithm, which the book derives from it.

These are classical results, proved in the 1950s and 1960s. On Prove2Me, Padberg and Rao's odd-cut results take an odd cut-tree as a hypothesis and do not construct one. Minimum-spanning-tree exchange properties exist in other encodings (rooted parent functions, a list-scan Kruskal). No formal statement of the realizability theorem, of the triangle condition on flow functions, or of the condensation lemma is known on the platform. The work is to formalize the known proofs. They connect undirected maximal flows with the max-flow min-cut theorem, spanning-tree exchange arguments and cut submodularity, and every one of these is reusable on its own.

Difficulty

The obvious first step for Lemma 2.1 compares flows directly, and it does not work. The inequality is a statement about maxima, and a flow of value $\min[v(x, z), v(z, y)]$ from $x$ to $y$ cannot be assembled by concatenating an $x$–$z$ flow and a $z$–$y$ flow, because the two flows compete for the same arc capacities. Every statement here is about attained maxima of flow values, and nothing in the mission's statements supplies the max-flow min-cut theorem for undirected networks with the one-direction constraint $f(x, y)\,f(y, x) = 0$. A solver must bring that in. For Lemma 3.1, the two networks have different node types, so flows have to be transported between them in both directions, and the naive way of pushing a flow forward into the condensed network can lose value. For Theorem 1.1, necessity is a single exchange, but sufficiency is not: the book itself remarks that it is "not obvious".

Formalization scope

Nodes are a Fintype with decidable equality. Arcs are a Mathlib SimpleGraph, so they are undirected and loop-free with at most one arc per pair. Capacities are a symmetric real function, nonnegative on arcs. Flows are real functions on ordered pairs that satisfy the book's constraints (10.1) of Chapter I. The maximal flow value is an attained maximum (IsGreatest), never a bare supremum. A flow function $v : N \to N \to \mathbb R$ is constrained only off the diagonal, matching the book's "$v(x, x)$ undefined", so (2.1) is quantified over pairwise distinct nodes. The book's alternative convention $v(x, x) = \infty$ is not used. Extending $v$ by $0$ on the diagonal would break (2.1) at $z = x$. The goal and Lemma 2.2 assume $v \ge 0$ off the diagonal. The book leaves this implicit (flow values are nonnegative), and without it the "if" direction fails for $v \equiv -1$. The goal assumes $N$ nonempty, because a tree is connected. "Realizable by a tree" means the network's graph is a tree on all of $N$. Some tree arcs may have capacity $0$. The condensed network has node type Option X, where none is the condensed node. Spanning subtrees are subgraphs $T \le G$ with T.IsTree. Lengths are a function on unordered pairs, and "the chain of in-tree arcs" is any path in $T$, which is unique.

A trivializing formalization is excluded. The flow function is defined by actual flows, never by path minima in a tree or by cut capacities. Realizability is the existence of a network whose flows have those maximal values, never a restatement of (2.1).

Not included: Lemma 3.2 and Theorem 4.1. Both concern objects that the book defines by a construction ("the final tree $T$" of the Gomory–Hu procedure, and the network $G^*$ of §4), and stating them faithfully would require formalizing those constructions. Contributions welcome: an undirected max-flow min-cut theorem in this encoding, the tree-network flow computation, and a formal Gomory–Hu construction for a later mission.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, RAND Corporation Report R-375-PR, 1962; Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
• R. E. Gomory and T. C. Hu, Multi-terminal network flows, Journal of the Society for Industrial and Applied Mathematics 9 (1961), 551–570. https://doi.org/10.1137/0109047
• J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proceedings of the American Mathematical Society 7 (1956), 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• R. C. Prim, Shortest connection networks and some generalizations, Bell System Technical Journal 36 (1957), 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
• M. W. Padberg and M. R. Rao, Odd minimum cut-sets and b-matchings, Mathematics of Operations Research 7 (1982), 67–80. https://doi.org/10.1287/moor.7.1.67

Motivation

An $m \times n$ matrix of $0$'s and $1$'s is the incidence matrix of $m$ sets against $n$ elements, or the adjacency matrix of a bipartite graph, or, when $m = n$, the adjacency matrix of a directed graph on $n$ nodes. The first question about such matrices is when one exists with prescribed row and column sums. Gale (1957) and Ryser (1957) answered it independently with a partial-sum criterion against the conjugate sequence. Ore (1956) solved the companion problem for directed graphs: when does a given directed graph have a subgraph with prescribed in- and out-degrees? Fulkerson (1960) treated the square case in which $1$'s are forbidden on the main diagonal, which is the degree problem for directed graphs without loops.

Ford and Fulkerson's Flows in Networks derives all of these from the supply-demand theorem for network flows. Chapter II, §11 states a two-sided version of Ore's theorem (Theorem 11.1, Corollary 11.2). §12 states the Gale–Ryser theorem in inequality form (Theorem 12.1, Corollaries 12.2–12.3) and Fulkerson's zero-trace theorem (Theorem 12.4, Corollaries 12.5–12.6). This mission formalizes those statements, citing the RAND typescript (Report R-375-PR, 1962), Chapter II, pp. 70–92.

Setting

A directed graph $G = [N; \mathcal A]$ has a finite node set $N$ and a set $\mathcal A$ of ordered pairs $(x, y)$ with $x \ne y$, at most one per ordered pair. A subgraph $H$ keeps the nodes and takes an arc set $\mathcal A' \subseteq \mathcal A$. Its local degree at $x$ is the pair $e_H(x)$, $i_H(x)$: the numbers of arcs of $H$ entering and leaving $x$. For $X \subseteq N$, $A(X)$ is the set of heads of arcs leaving $X$ and $B(X)$ the set of tails of arcs entering $X$; $|(X, y)|$ and $|(y, X)|$ count the arcs from $X$ to $y$ and from $y$ to $X$; $a(X) = \sum_{x \in X} a(x)$.

A $(0, 1)$-matrix $A = (a_{ij})$ has every entry $0$ or $1$. For nonnegative integers $a_1, \dots, a_m$ the conjugate sequence is $a^*_j = |\{ i \mid a_i \ge j \}|$. For nonnegative integers $a_1, \dots, a_n$, the diagonally restricted conjugate sequence $(a^{**}_k)$ is defined as follows. In an $n \times n$ array, row $i$ places $a_i$ dots in its leftmost columns other than column $i$, and $a^{**}_k$ is the number of dots in column $k$:

$$a^{**}_k = |\{ i \mid i < k,\ a_i \ge k - 1 \}| + |\{ i \mid i > k,\ a_i \ge k \}|.$$

For $a = (4, 3, 3, 2, 2, 1)$ this gives $a^{**} = (5, 4, 2, 3, 1, 0)$, which is not monotone.

In Lean these are Digraph, IsSubgraph, outDeg, inDeg, succSet, predSet, numArcsTo, numArcsFrom (file Def_FlowsNetworks_Matrices_Digraph) and IsZeroOne, conj, diagDot, diagConj (file Def_FlowsNetworks_Matrices_ZeroOne), all in the namespace FlowsNetworks.Matrices.

Formalization targets

Goal: the zero-trace theorem (Chapter II, Theorem 12.4, p. 89)

For nonnegative integers $a_1 \ge \dots \ge a_n$ and $b_1 \ge \dots \ge b_n$, there is an $n \times n$ $(0, 1)$-matrix with

$$\sum_j a_{ij} \le a_i, \qquad \sum_i a_{ij} \ge b_j, \qquad \sum_i a_{ii} = 0$$

if and only if

$$\sum_{i=1}^k b_i \le \sum_{i=1}^k a^{**}_i, \qquad k = 1, \dots, n.$$

Milestones

1. Theorem 11.1 (pp. 73–74). For integers $0 \le a(x) \le a'(x)$ and $0 \le b(x) \le b'(x)$, $G$ has a subgraph with $a \le i_H \le a'$ and $b \le e_H \le b'$ iff, for all $X \subseteq N$,

$$a(X) \le \sum_{y \in A(X)} \min[b'(y), |(X, y)|], \qquad b(X) \le \sum_{y \in B(X)} \min[a'(y), |(y, X)|].$$

2. Corollary 11.2 (Ore, pp. 74–75): exact degrees $i_H = a$, $e_H = b$ iff $a(N) = b(N)$ and the first inequality holds with $b$ in place of $b'$.
3. Theorem 12.1 (pp. 79–80). For nonnegative integers $a_1, \dots, a_m$ and $b_1 \ge \dots \ge b_n$, an $m \times n$ $(0, 1)$-matrix with $\sum_i a_{ij} \ge b_j$ and $\sum_j a_{ij} \le a_i$ exists iff $\sum_{j \le k} b_j \le \sum_{j \le k} a^*_j$ for $k = 1, \dots, n$.
4. Corollaries 12.2 and 12.3 (p. 80): the cases $b_j = b$ (criterion $nb \le \sum_j a^*_j$) and $a_i = a$ (criterion $\sum_j b_j \le ma$, $b_j \le m$).
5. Corollaries 12.5 and 12.6 (p. 90): the zero-trace cases $b_i = b$ (criterion $nb \le \sum_i a^{**}_i$) and $a_i = a$ (criterion $\sum_i b_i \le na$, $b_i \le n - 1$).

Significance

The result itself. Theorem 12.4 characterizes the out-degree upper bounds and in-degree lower bounds that a loopless directed graph on $n$ labelled nodes can meet. With equal totals, it characterizes the degree sequences of such graphs (directed graphs with no loops and no parallel arcs). Theorem 12.1 is the inequality form of the Gale–Ryser theorem, which underlies the theory of the class $\mathfrak A(R, S)$ of $(0, 1)$-matrices with given margins: Ryser's structure matrix, interchanges, and term rank. Ore's theorem is its counterpart for an arbitrary host graph. Corollaries 12.2–12.3 and 12.5–12.6 are the closed forms used in scheduling and seating problems, such as $n$ families at $m$ tables with no two relatives at one table.

Formalizing it. All results are classical and proved. On the platform, the Gale–Ryser theorem exists only as AppliedComb.ManyFaces.gale_ryser (Keller–Trotter, Theorem 16.12). That statement requires equal sums and exact margins, sorts both sequences, and requires positive parts. The book's version has one-sided bounds, arbitrary totals, an unsorted $a$ and zero entries, so it is drafted here, not referenced. No zero-trace theorem, diagonally restricted conjugate, or directed-subgraph degree theorem was found on the platform.

Difficulty

Each criterion is a family of $n$ inequalities, and the content is that these few inequalities suffice. A direct argument has to show that a deficiency in some arbitrary set of columns, or of nodes, is already seen by an initial segment of the sorted sequence. The diagonal restriction breaks the usual monotonicity: $a^{**}$ need not be monotone (the example above has $a^{**}_3 < a^{**}_4$), so the standard exchange argument for conjugate sequences does not apply unchanged. The ordering hypotheses are essential. Without $b_1 \ge \dots \ge b_n$ both Theorem 12.1 and Theorem 12.4 are false (findings F1, F2: $a = (2)$, $b = (0, 2)$ for 12.1; $a = (1, 1)$, $b = (0, 2)$ for 12.4). The existence side needs an integral object (a matrix or a subgraph), not a fractional one.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℕ with entries at most $1$. Every integer datum is a natural number, so nonnegativity is built in. Indices are $0$-based: the book's index $i$ is i + 1, and $\sum_{i=1}^k$ is the sum over i.val < k. Orderings are Antitone. Zero trace is written $\sum_i a_{ii} = 0$, as printed. Directed graphs have a finite node type with decidable equality, arcs form a Finset (N × N) with no loops, and a subgraph is an arc set $H \subseteq \mathcal A$. Corollaries 12.3, 12.5 and 12.6 carry the ordering hypotheses of the theorem they specialize. In Corollary 11.2 the page prints $b'(y)$ in (11.19), which is read as $b(y)$ because the corollary prescribes exact degrees. Its summation range, printed $y \in A(x)$, is read as $A(X)$, as in (11.14).

The trivializing formalization is ruled out: $a^*$ and $a^{**}$ are explicit counts computed from the integers $a_i$, never defined through the existence of a matrix, and every partial-sum criterion is required for every $k = 1, \dots, n$, not only for $k = n$.

Beyond the paper. Two sharpness probes accompany the faithful statements. Each is expected to be false, and a disproof is the sought outcome. zero_one_matrix_existence_probe is Theorem 12.1 without $b_1 \ge \dots \ge b_n$ (F1: $m = 1$, $a = (2)$, $b = (0, 2)$ satisfies the criterion but admits no matrix). zero_trace_theorem_probe is Theorem 12.4 without $b_1 \ge \dots \ge b_n$ (F2: $n = 2$, $a = (1, 1)$, $b = (0, 2)$ likewise).

A complete development needs integral network-flow feasibility (the supply-demand theorem with integrality, or a direct combinatorial substitute), the bijection between integral flows on a bipartite network and $(0, 1)$-matrices or subgraphs, and conjugate-sequence identities such as $\sum_i \min(a_i, k) = \sum_{j \le k} a^*_j$. These pieces are reusable for the rest of Chapter II. Direct combinatorial proofs that avoid flows are equally welcome.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, The RAND Corporation, Report R-375-PR, 1962; Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
• D. Gale, A theorem on flows in networks, Pacific Journal of Mathematics 7 (1957), 1073–1082. https://doi.org/10.2140/pjm.1957.7.1073
• H. J. Ryser, Combinatorial properties of matrices of zeros and ones, Canadian Journal of Mathematics 9 (1957), 371–377. https://doi.org/10.4153/CJM-1957-044-3
• O. Ore, Studies on directed graphs, I, Annals of Mathematics 63 (1956), 383–406. https://doi.org/10.2307/1970010
• D. R. Fulkerson, Zero-one matrices with zero trace, Pacific Journal of Mathematics 10 (1960), 831–836. https://doi.org/10.2140/pjm.1960.10.831

Why two capacities at a time

The value of a maximal flow is the basic output of network-flow models of transport, communication and supply systems. A planner who can enlarge the capacity of a link wants to know what the enlargement buys. For a single link the answer is simple. For two links it is a question about interaction: does enlarging one make enlarging the other more valuable (the links reinforce each other) or less valuable (they interfere)? L. S. Shapley answered it, and Ford and Fulkerson give his theorems and proofs in Section 13 of Chapter I of Flows in Networks. Any two arcs either always reinforce or always interfere, and in several positions the network's geometry alone decides which. These are early instances of supermodularity and submodularity of an optimal value in its parameters, a theme that later became central in parametric optimization and discrete convex analysis.

Setting

A network $[N;\mathcal A]$ is a finite set $N$ of nodes together with a set $\mathcal A$ of ordered pairs $(x,y)$ of distinct nodes, the arcs. The arc $(x,y)$ has initial node $x$ and terminal node $y$. There is at most one arc from $x$ to $y$, but $(x,y)$ and $(y,x)$ may both be arcs. The nodes are split into a set $S$ of sources, a disjoint set $T$ of sinks, and the remaining intermediate nodes $R$. Each arc carries a capacity $c(x,y)\ge0$.

A flow from $S$ to $T$ is a function $f$ on the arcs with $0\le f(x,y)\le c(x,y)$ on every arc, and with conservation $f(x,N)=f(N,x)$ at every intermediate node $x$. Here $f(x,N)$ is the total flow on arcs leaving $x$ and $f(N,x)$ the total on arcs entering it. Its value is the net amount leaving the sources, $v=f(S,N)-f(N,S)$. The maximal flow value $\bar v$ is the largest value of a flow. A node set $X$ containing every source and no sink determines the cut $(X,\bar X)$, the set of arcs from $X$ to its complement, with capacity $c(X,\bar X)$, the sum of their capacities.

Fix two distinct arcs $A_i$ and $A_j$ and keep every other capacity fixed and finite. Write $\bar v_i(\xi)$ for the maximal flow value when $c(A_i)$ is replaced by $\xi$, and $\bar v_{ij}(\xi,\eta)$ for the value when $c(A_i)$ and $c(A_j)$ are replaced by $\xi$ and $\eta$. These two capacities may also be $\infty$, and then $\bar v$ may be $\infty$. For a rectangle with corners $(\xi,\eta)$, $(\xi+h,\eta)$, $(\xi,\eta+k)$, $(\xi+h,\eta+k)$ in the nonnegative quadrant, with $hk\neq0$, the difference quotient is

$$q_{ij}=\frac{\bar v_{ij}(\xi+h,\eta+k)-\bar v_{ij}(\xi+h,\eta)-\bar v_{ij}(\xi,\eta+k)+\bar v_{ij}(\xi,\eta)}{hk}.$$

The interaction constant is

$$p_{ij}=\bar v_{ij}(\infty,\infty)-\bar v_{ij}(0,\infty)-\bar v_{ij}(\infty,0)+\bar v_{ij}(0,0),$$

which may be $+\infty$, or indeterminate ($\infty-\infty$).

Formalization targets

Goal: Theorem 13.1, one sign

$$\Bigl(\forall\,\text{rectangles: } q_{ij}\ge0\Bigr)\ \lor\ \Bigl(\forall\,\text{rectangles: } q_{ij}\le0\Bigr).$$

The goal leaves the sign open. Which sign occurs depends on the whole network: in the book's Fig. 13.3, removing a third arc turns $p_{12}=1$ into $p_{12}=-1$.

Milestones

1. Eq. (13.1). $\bar v=\min\{c(X,\bar X): S\subseteq X,\ T\cap X=\emptyset\}$, the max-flow min-cut theorem for several sources and sinks.
2. Eq. (13.2). $\bar v_i(\xi)=\min[\bar v_i(0)+\xi,\ \bar v_i(\infty)]$ for $\xi\in[0,\infty]$.
3. Eq. (13.4). $\bar v_{ij}(\xi,\eta)=\min[\bar v_{ij}(0,0)+\xi+\eta,\ \bar v_{ij}(0,\infty)+\xi,\ \bar v_{ij}(\infty,0)+\eta,\ \bar v_{ij}(\infty,\infty)]$.
4. Corollary 13.2. If $p_{ij}>0$ (including $+\infty$), $q_{ij}$ is sometimes $>0$ and never $<0$. If $p_{ij}=0$ or $p_{ij}$ is indeterminate, $q_{ij}\equiv0$. If $p_{ij}<0$, $q_{ij}$ is sometimes $<0$ and never $>0$.
5. Theorem 13.3. $q_{ij}\ge0$ when the terminal node of $A_i$ is the initial node of $A_j$. $q_{ij}\le0$ when $A_i$ and $A_j$ share their initial node. $q_{ij}\ge0$ when $A_i$ starts at a source and $A_j$ ends at a sink.
6. Corollary 13.4. $q_{ij}\le0$ when $A_i$ and $A_j$ share their terminal node, when both start at sources, or when both end at sinks.

Corollary 13.2 refines the goal by naming the sign. Theorem 13.3 and Corollary 13.4 fix the sign from positions alone.

Significance

Theorem 13.1 says that the cross effect of two capacities on the maximal flow value never changes sign. The marginal value of capacity on one arc is monotone in the capacity of the other, in a direction fixed once and for all by the network. Corollary 13.2 reduces that direction to a single number computed from four maximal-flow values at the corners $0$ and $\infty$. Theorem 13.3 and Corollary 13.4 show that some directions are forced by position: arcs in series reinforce, and arcs that compete at a common node interfere. These facts underlie sensitivity analysis of maximal flows. They are also the two-parameter case of the lattice and submodularity structure of minimal cuts.

The theorems were proved by Shapley and printed with proofs by Ford and Fulkerson (RAND, 1962). Their proofs argue from a picture of how the regions of linearity of $\bar v_{ij}$ can sit in the quadrant (Fig. 13.2). No machine-checked proof of any statement of Section 13 exists on Prove2Me. Proved max-flow min-cut statements exist there for a single source and sink and in other conventions, and are related to milestone 1 rather than identical to it. Formalizing the section gives a checked account of the parametric behaviour of the maximal flow value. That includes the infinite capacities the section allows, and the indeterminate case of $p_{ij}$, which a picture handles only informally.

Difficulty

The first idea is to read the sign off formula (13.4): $\bar v_{ij}$ is the minimum of four affine functions, so its mixed second difference is determined by which pieces are active at the four corners of a rectangle. A minimum of four arbitrary affine functions, however, can have mixed differences of both signs. The claim depends on constraints that the four corner values satisfy because they come from one network, and on how the regions of linearity can meet. The book's proof uses a case analysis of these configurations: at most one diagonal boundary segment, and its slope fixed by $p_{ij}$. Making that analysis rigorous, including the degenerate configurations where regions are empty or corner values are infinite, is the core of the goal and of Corollary 13.2.

Milestone 1 also has to be established in the several-source form, with arcs allowed to enter sources and to leave sinks, where the reduction to a single source and sink must respect flows whose sources have net inflow.

Formalization scope

Nodes form a finite type with decidable equality; arcs are a finite set of ordered pairs without loops; sources and sinks are disjoint finite sets, either of which may be empty (then $\bar v\equiv0$ and every statement holds trivially, as in the book). Capacities of the fixed arcs are finite nonnegative reals. The two varied capacities and every maximal flow value lie in $[0,\infty]$ (ℝ≥0∞). A flow is a real function vanishing off the arcs, and the maximal flow value is the supremum of flow values in $[0,\infty]$. That supremum is taken over a nonempty set (the zero flow), so it is never a default value, and it is $\infty$ exactly when flow values are unbounded. The maximal flow value is not defined as a minimum cut capacity; equality with the minimum cut is milestone 1.

The difference quotient is taken at finite real arguments over every rectangle with $\xi,\eta,\xi+h,\eta+k\ge0$ and $hk\neq0$; $h$ and $k$ may be negative. The book prints the third term of (13.12) as $\bar v_{ij}(\xi,\eta+h)$. The rectangle the theorem names needs $\bar v_{ij}(\xi,\eta+k)$, which is the formalized quotient; with the printed term the claim already fails for two arcs in series. The constant $p_{ij}$ is a four-way value (indeterminate, $+\infty$, $-\infty$, real), so $\infty-\infty$ is never silently assigned a number.

"Of one sign" is formalized as one sign for all rectangles at once. The rectangle-by-rectangle reading, under which every real number is trivially $\ge0$ or $\le0$, is ruled out.

A complete development needs flows with several sources and sinks, cuts, and the max-flow min-cut theorem in that form; the definitions here are self-contained and reusable for any parametric max-flow statement. Contributions of the general piecewise-linear structure of $\bar v$ in one or two capacities are welcome.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, The RAND Corporation, Report R-375-PR, 1962, Chapter I, §§7 and 13; published by Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• D. M. Topkis, Minimizing a submodular function on a lattice, Operations Research 26 (1978), 305–321. https://doi.org/10.1287/opre.26.2.305

Motivation

The maximal flow problem asks how much of a commodity can be sent from one node of a network to another when every arc has a capacity. It was posed in the 1950s in the study of rail networks, and its answer, the max flow min cut theorem of L. R. Ford, Jr. and D. R. Fulkerson, became the organizing result of combinatorial optimization: the bottleneck of a network, a cheapest set of arcs separating the two terminals, has exactly the capacity of the best flow. Chapter I of Ford and Fulkerson's Flows in Networks is the canonical exposition. This mission formalizes Chapter I, §§1–9, in the RAND typescript of the book (Report R-375-PR, 1962), whose numbering is used throughout.

Timeline. Ford and Fulkerson proved the theorem in 1956 for undirected networks in an arc–chain formulation ("Maximal flow through a network", Canadian J. Math.); Elias, Feinstein and Shannon gave an independent proof the same year (IRE Trans. Inf. Theory). The book restates the theory for directed networks with node–arc flows, which is the form used in all later applications and the form formalized here.

Setting

A network $[N; \mathcal A]$ is a finite set $N$ of nodes together with a set $\mathcal A$ of ordered pairs $(x, y)$ of distinct nodes, the arcs. At most one arc leads from $x$ to $y$, but both $(x, y)$ and $(y, x)$ may be arcs. Each arc has a capacity $c(x, y) \ge 0$, a real number. For node sets $X, Y$, $(X, Y)$ is the set of arcs from $X$ to $Y$, and $g(X, Y)$ is the sum of a function $g$ over those arcs; $\bar X = N - X$.

Fix two distinct nodes, the source $s$ and the sink $t$. A flow of value $v$ from $s$ to $t$ is a function $f$ on the arcs with $0 \le f(x, y) \le c(x, y)$ such that the net flow out of every node, $\sum_{y} f(x, y) - \sum_{y} f(y, x)$, is $v$ at $s$, $-v$ at $t$, and $0$ elsewhere. A flow is maximal if no flow has larger value. A node set $X$ with $s \in X$, $t \in \bar X$ determines the cut $(X, \bar X)$ separating $s$ and $t$, of capacity $c(X, \bar X)$; a minimal cut has least capacity.

A flow augmenting path with respect to $f$ is a sequence of distinct nodes from $s$ to $t$ in which each consecutive pair is joined either by a forward arc with $f < c$ or by a reverse arc with $f > 0$. The source set $X$ of a flow is the smallest node set containing $s$ and closed under such steps; the sink set $\bar Y$ is the smallest node set containing $t$ and closed under such steps taken backwards. With lower bounds $\ell$, $0 \le \ell \le c$, the bounds $0 \le f \le c$ are replaced by $\ell \le f \le c$.

Formalization targets

Goal: Theorem 5.1 (p. 19), the max flow min cut theorem

$$\max\{v : \text{there is a flow of value } v \text{ from } s \text{ to } t\} \;=\; \min\{c(X, \bar X) : s \in X,\ t \in \bar X\},$$

with both extrema attained. The goal fixes nothing beyond the book's hypotheses: any finite network, any nonnegative real capacities.

Milestones, in attack order

1. Lemma 4.1 (p. 18): for every flow of value $v$ and every cut, $v = f(X, \bar X) - f(\bar X, X) \le c(X, \bar X)$.
2. Corollary 5.2 (p. 22): a flow is maximal if and only if there is no flow augmenting path.
3. Corollary 5.3 (p. 23): a cut is minimal if and only if every maximal flow saturates its forward arcs and leaves its backward arcs flowless.
4. Corollary 5.4 (p. 23): if $X$ and $Y$ give minimal cuts, so do $X \cup Y$ and $X \cap Y$.
5. Theorem 5.5 (p. 23): the source set of any maximal flow is contained in the source side of every minimal cut.
6. Theorem 5.6 (p. 25): with strictly positive capacities, the minimal cut is unique if and only if the source-set cut and the sink-set cut have the same arcs.
7. Theorem 8.1 (p. 34, integrity theorem): integral capacities admit an integral maximal flow.
8. Theorem 9.2 (p. 39): with lower bounds $\ell$, if a feasible $f$ exists, the minimal value of $v$ equals $\max_X \big(\ell(X, \bar X) - c(\bar X, X)\big)$.

Significance

The result itself. The theorem converts an optimization over a continuum of flows into a finite minimum over node sets, and the integrity theorem makes the conversion combinatorial. The later chapters of the book derive from these two results the supply–demand and circulation theorems, the König–Egerváry theorem, Menger's theorem, Dilworth's theorem and Hall's theorem on distinct representatives. Corollary 5.2 is the correctness criterion of every augmenting-path algorithm, and Corollaries 5.3–5.4 and Theorems 5.5–5.6 describe the lattice of minimal cuts that later work on parametric flows and cut enumeration uses.

Formalizing it. The theorem is proved, and several machine-checked versions exist on this platform in other conventions: FordFulkerson56.MinCut.minimal_cut_theorem (the 1956 undirected arc–chain form), AppliedComb.Flows.max_flow_min_cut and AppliedComb.Flows.integral_max_flow (networks without 2-cycles and without arcs into the source or out of the sink), LinearOptimization.max_flow_min_cut (positive extended-real capacities, parallel arcs), VanderbeiLP.Networks.max_flow_min_cut (value measured on a return arc), and the augmenting-path criteria GoldbergTarjan.Generic.max_flow_iff_no_augmenting_path and EdmondsKarp.ShortestPath.isMaxFlow_iff_no_augPath. None states the book's node–arc theorem for directed networks in which antiparallel arcs, arcs into the source and zero capacities are all allowed. This mission states it in exactly the book's conventions, together with the minimal-cut structure theory of §5 and the lower-bound form of §9, which have no platform counterpart.

Difficulty

The inequality "max flow $\le$ min cut" holds for every pair of a flow and a cut and is routine. The difficulty is the reverse inequality together with attainment: the theorem asserts that a maximal flow exists, and this is not free over the reals. The labeling method of §8 need not terminate when capacities are irrational: the book gives a network in §8 where it converges to a flow of value one quarter of the maximum. So an argument that only runs the algorithm covers rational or integral data and leaves the general statement open. Theorems 5.5 and 5.6 add reasoning about inductively defined node sets and about arc sets rather than node sets: two different node sets can determine the same cut, which is why Theorem 5.6 compares arc sets and needs $c > 0$.

Formalization scope

Nodes are a Fintype with decidable equality; arcs a Finset (N × N) with no loops; capacities and flows functions $N \to N \to \mathbb R$, flows required to vanish off $\mathcal A$ and to be nonnegative on it. Capacities are finite reals throughout. The source and sink are distinct ($s \neq t$), the book's "two distinguished nodes". A cut is given by its node set $X$; where the book compares cuts (Theorem 5.6) the Lean compares the arc sets $(X, \bar X)$. Every maximum and minimum is stated as attained (IsGreatest, IsLeast) or through explicit "maximal flow" and "minimal cut" predicates; no sSup or sInf appears. The source and sink sets are defined as intersections of all node sets closed under the book's rules (a), (b) and (a′), (b′), not through a reachability algorithm.

The statement admits a trivializing formalization that is ruled out here: defining the maximal flow value as the minimal cut capacity, or minimal cuts through flow values, or replacing $c \ge 0$ by $c = 0$; flows, cuts, maximality and minimality are each defined from the network alone.

Beyond the paper. Two variant items accompany the faithful statements. A strengthening of Corollary 5.3: one flow, not assumed maximal, that saturates $(X, \bar X)$ and is zero on $(\bar X, X)$ already makes the cut minimal and the flow maximal, since by Lemma 4.1 its value equals the cut capacity. A sharpness probe for Theorem 5.6: the statement with $c > 0$ weakened to $c \ge 0$, which the book's Fig. 5.2 shows to be false (two arcs, capacities 1 and 0, give two minimal cuts while the source-set and sink-set cuts coincide); a disproof is the sought outcome.

A complete development needs finite sums over arc sets and their splitting along $N = X \cup \bar X$ (the identities (3.3)–(3.4)), compactness of the flow polytope or an augmenting-path argument, and an inductive closure argument for the source set. The network, flow and cut definitions are reusable by the rest of this series (circulations, dynamic flows, flow functions) and by any formalization of matching or connectivity theorems through flows. Proofs by either route, compactness or the labeling method with integrality, are welcome.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, The RAND Corporation, Report R-375-PR, 1962; Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• P. Elias, A. Feinstein and C. E. Shannon, A note on the maximum flow through a network, IRE Transactions on Information Theory 2 (1956), 117–119. https://doi.org/10.1109/TIT.1956.1056816

Motivation

Many questions in operations research and combinatorics ask whether a system of linear inequalities on a network has a solution: can the demands at a set of warehouses be met from the supplies at a set of factories through roads of limited capacity; is there a nonnegative matrix with bounded entries whose row and column sums lie between given limits; can a periodic schedule be met when every activity has a minimum and a maximum rate. Chapter II of L. R. Ford, Jr. and D. R. Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962, doi:10.1515/9781400875184) answers these questions by feasibility theorems: a system of flow constraints has a solution exactly when a family of inequalities, one for each set of nodes, holds.

The history in the chapter's first three sections is short. D. Gale proved the supply-demand theorem in 1957 (A theorem on flows in networks, Pacific J. Math. 7 (1957) 1073–1082). A. J. Hoffman proved the circulation theorem, with lower and upper bounds on every arc, in 1960 (Some recent applications of the theory of linear inequalities to extremal combinatorial analysis, Proc. Sympos. Appl. Math. 10, AMS, 1960), originally through the separation theorem for convex sets. Ford and Fulkerson derive all of these, and the two-sided variants, from the max flow min cut theorem of their Chapter I.

Setting

A network $[N; \mathcal A]$ is a finite set $N$ of nodes together with a set $\mathcal A$ of ordered pairs $(x, y)$ of distinct nodes, the arcs; there is at most one arc from $x$ to $y$, but both $(x, y)$ and $(y, x)$ may be arcs. Each arc carries a real capacity $c(x, y) \ge 0$. For a real function $g$ on the arcs and node sets $X, Y \subseteq N$,

$$g(X, Y) = \sum_{(x, y) \in \mathcal A,\ x \in X,\ y \in Y} g(x, y),$$

so $f(x, N)$ is the total of $f$ on arcs leaving $x$ and $f(N, x)$ the total on arcs entering $x$. For a node set $X$, $\bar X = N - X$; for a node function $a$, $a(X) = \sum_{x \in X} a(x)$.

In §§1–2 the nodes are partitioned into sources $S$, intermediate nodes $R$ and sinks $T$ (any of them may be empty). Sources carry a supply $a(x) \ge 0$, sinks a demand $b(x) \ge 0$. A function $f$ on the arcs is a feasible flow for the supply-demand problem when the net outflow $f(x, N) - f(N, x)$ is at most $a(x)$ at every source, zero at every intermediate node, the net inflow $f(N, x) - f(x, N)$ is at least $b(x)$ at every sink, and $0 \le f \le c$ on every arc.

In §3 there are no distinguished nodes. A lower bound function $\ell$ with $0 \le \ell \le c$ is given on the arcs, and a feasible circulation is a function $f$ on the arcs with

$$f(x, N) - f(N, x) = 0 \ \ (x \in N), \qquad \ell(x, y) \le f(x, y) \le c(x, y) \ \ ((x, y) \in \mathcal A).$$

Formalization targets

Goal: Hoffman's circulation theorem (Chapter II, Theorem 3.1, p. 26)

For a network with capacities $c$ and lower bounds $0 \le \ell \le c$, a feasible circulation exists if and only if

$$c(X, \bar X) \ge \ell(\bar X, X) \quad \text{for all } X \subseteq N.$$

Milestones

1. Theorem 1.1 (p. 4), Gale's supply-demand theorem. The supply-demand constraints are feasible if and only if $b(T \cap \bar X) - a(S \cap \bar X) \le c(X, \bar X)$ for every $X \subseteq N$.
2. Corollary 1.2 (p. 7). They are feasible if and only if for every $T' \subseteq T$ some flow respecting the supplies, conservation and capacities delivers $f_{T'}(N, T') - f_{T'}(T', N) \ge b(T')$.
3. Theorem 2.1 (p. 21). With two-sided bounds $0 \le a \le a'$ on the net outflow at sources and $0 \le b \le b'$ on the net inflow at sinks, feasibility holds if and only if, for all $X \subseteq N$,

$$c(X, \bar X) \ge b(T \cap \bar X) - a'(S \cap \bar X), \qquad c(X, \bar X) \ge a(S \cap X) - b'(T \cap X).$$

4. Corollary 2.2 (p. 22). The two-sided system is feasible if and only if each of the two one-sided systems (lower bound at sources with upper bound at sinks; upper bound at sources with lower bound at sinks) is feasible.
5. Corollary 2.3 (p. 23). For $0 \le a_i \le a'_i$, $0 \le b_j \le b'_j$, $c_{ij} \ge 0$: if one $m \times n$ matrix meets $a_i \le \sum_j f_{ij}$, $\sum_i f_{ij} \le b'_j$ and another meets $\sum_j f_{ij} \le a'_i$, $b_j \le \sum_i f_{ij}$, both with $0 \le f_{ij} \le c_{ij}$, then a single matrix meets all four row and column limits with $0 \le f_{ij} \le c_{ij}$.
6. Theorem 3.2 (p. 28). With node bounds $a \le a'$ (no sign condition) on the net inflow $f(N, x) - f(x, N)$ at every node and arc bounds $0 \le \ell \le c$, feasibility holds if and only if

$$c(X, \bar X) \ge \ell(\bar X, X) + \max\,[a(\bar X), -a'(X)] \quad \text{for all } X \subseteq N.$$

With $a = a' = 0$ this is the goal.

Significance

The circulation theorem is the most general of the chapter's feasibility criteria for directed networks: the supply-demand theorem, the existence of $s$–$t$ flows between lower and upper arc bounds (Chapter I, §9), and the transportation-matrix criterion of Corollary 2.3 all follow from it or from its extension, Theorem 3.2, by adjoining arcs, and the rest of Chapter II applies them to systems of distinct representatives and (0, 1)-matrices.

All results of the mission have been proved for more than sixty years. None of them, in this form, is formalized on Prove2Me: the platform has decomposition results for circulations and max flow min cut statements in other conventions, but no Gale or Hoffman feasibility criterion. The mission produces machine-checked versions of the six numbered results and the goal over one shared notion of network, in the book's notation.

Difficulty

Necessity is the routine half of every theorem. Sufficiency asks for a flow built from a family of $2^{|N|}$ inequalities, one per node set, and constructing a flow arc by arc or node by node with local repairs gives no argument that the repairs stop or that all constraints hold at once. The statements also differ in ways that are easy to get wrong: §§1–2 bound the net outflow at sources but the net inflow at sinks, §3 bounds the net inflow everywhere, the node bounds of Theorem 3.2 carry no sign condition and may be negative, and Theorem 2.1 needs two inequalities per node set rather than one. Real-valued data rule out any argument by induction on integer flow values without a separate limiting step.

Formalization scope

Nodes form a Fintype with decidable equality; arcs are a Finset (N × N) with no loops; capacities and flows are real functions $N \to N \to \mathbb R$. A flow is required to vanish off $\mathcal A$, and every sum $g(X, Y)$ runs over arcs only, so the values of $c$ and $\ell$ off $\mathcal A$ never matter. Supplies, demands and node bounds are real functions on all of $N$ whose values enter only through sums over the sets the book names ($S \cap \bar X$, $T \cap X$, …). The partition $S, R, T$ is three pairwise disjoint Finsets covering $N$. $X$ ranges over all subsets of $N$, including $\emptyset$ and $N$. Each section's sign convention is copied: §§1–2 bound the net outflow at sources and the net inflow at sinks, §3 bounds the net inflow. Corollary 2.3 is stated for real matrices indexed by Fin m × Fin n. All data are finite reals; no integrality is assumed.

Feasibility is always stated as the existence of a function on the arcs satisfying the book's displayed constraints. Defining feasibility through the cut condition itself, or through a linear-programming solver predicate, would make every theorem definitional and is ruled out.

Beyond the paper. One variant is posed beside the faithful goal: [Strengthened] Theorem 3.1, the circulation theorem for any real lower bound $\ell \le c$ without $\ell \ge 0$ (capacities stay nonnegative). The substitution $g = f - \ell$ reduces it to a supply-demand problem with nonnegative capacities $c - \ell$, whose Gale condition is $c(X, \bar X) \ge \ell(\bar X, X)$ regardless of the sign of $\ell$; it implies the faithful statement.

A complete development needs Chapter I's max flow min cut theorem in some form (or the linear-programming duality theorem, or Farkas' lemma), the manipulation of arc sums over node sets, and the auxiliary-network constructions. The definitions of networks, arc sums and partitions are reusable by the later Chapter II missions. Proofs of any milestone, of the variant, and alternative proofs through LP duality are welcome.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, The RAND Corporation, Report R-375-PR, 1962; Princeton University Press, 1962. doi:10.1515/9781400875184
• D. Gale, A theorem on flows in networks, Pacific Journal of Mathematics 7 (1957), 1073–1082. doi:10.2140/pjm.1957.7.1073
• A. J. Hoffman, Some recent applications of the theory of linear inequalities to extremal combinatorial analysis, Proceedings of Symposia in Applied Mathematics 10, American Mathematical Society, 1960, 113–127.
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. doi:10.4153/CJM-1956-045-5

Motivation

A convex program whose objective and feasible set are known only through oracles, routines that answer queries about one point at a time, can still be solved to any prescribed accuracy with a number of queries bounded in advance. The ellipsoid method is the classical algorithm that achieves this. It was introduced for convex minimization by Yudin and Nemirovski (Ekonomika i Matematicheskie Metody, 1976) and by Shor (Cybernetics, 1977), and it became widely known when Khachiyan used it to prove that linear programming is solvable in polynomial time (Soviet Math. Dokl., 1979). Grötschel, Lovász and Schrijver turned the method into a general tool of combinatorial optimization, the equivalence of separation and optimization (Springer, 1988).

Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001) present the method in §5.2 as the engine of their theorem that convex programs are polynomially solvable, and prove an explicit, fully quantified complexity bound for it, Theorem 5.2.1. This mission is the tenth of a series formalizing the book's main results and covers §5.2 (pp. 342–352).

Setting

Vectors are elements of $\mathbb R^n$, $n \ge 2$, with the Euclidean norm $\|x\|_2 = \sqrt{x^Tx}$. The problem is

$$\min_x\{f(x) : x \in X \subset \mathbb R^n\} \tag{5.2.9}$$

where $f : \mathbb R^n \to \mathbb R$ is convex and $X$ is a closed, bounded, convex set with nonempty interior. Two radii $r, R > 0$ are known in advance (assumption A): $X$ lies in the ball $E_0 = \{x \mid \|x\|_2 \le R\}$ and contains some ball $\{x \mid \|x - \bar x\|_2 \le r\}$, whose centre $\bar x$ is not known.

The data are accessed through two oracles. A separation oracle for $X$ answers a query $x$ by "$x \in X$" when that holds, and otherwise returns a vector $a \ne 0$ with $a^Tx \ge a^Ty$ for all $y \in X$. A first order oracle for $f$ returns $f(x)$ and a subgradient $\eta$ of $f$ at $x$: $f(y) \ge f(x) + \eta^T(y - x)$ for all $y$.

An ellipsoid is $E(c, B) = \{c + Bu \mid u^Tu \le 1\}$ with $\operatorname{Det} B \ne 0$. For $a \ne 0$, put $p = B^Ta/\sqrt{a^TBB^Ta}$ and

$$c^+ = c - \frac{1}{n+1}Bp,\qquad B^+ = \frac{n}{\sqrt{n^2-1}}B + \Big(\frac{n}{n+1} - \frac{n}{\sqrt{n^2-1}}\Big)(Bp)p^T .$$

The ellipsoid method with accuracy $\epsilon > 0$ starts from $c_0 = 0$, $B_0 = RI$, $L_0 = 0$. At step $t = 1, 2, \dots$ it queries the separation oracle at $c_{t-1}$. If a separator $a$ is returned, the step is nonproductive, $a_t = a$ and $L_t = L_{t-1}$. Otherwise the step is productive: the first order oracle is queried at $c_{t-1}$; a zero subgradient stops the method with result $c_{t-1}$; a nonzero one becomes $a_t$, and $L_t = \max\{L_{t-1}, R\|a_t\|_2 - a_t^Tc_{t-1}\}$. Then $c_t = c_{t-1}^+$, $B_t = B_{t-1}^+$ (computed from $a_t$), $\rho_t = |\operatorname{Det} B_t|^{1/n}$, and the method stops if

$$\frac{\rho_t}{r} < \frac{\epsilon}{L_t + \epsilon}, \tag{5.2.17}$$

returning the productive search point $c_{\tau-1}$, $\tau \le t$, with the smallest value of $f$. Finally $\operatorname{Var}_R(f) = \max_{E_0} f - \min_{E_0} f$.

Formalization targets

Goal: Theorem 5.2.1 (p. 349)

For every accuracy $\epsilon > 0$, every separation oracle for $X$ and every first order oracle for $f$, the ellipsoid method terminates after no more than

$$N(\epsilon) = \operatorname{Ceil}\Big(2n^2\Big[\ln\Big(\frac Rr\Big) + \ln\Big(\frac{\epsilon + \operatorname{Var}_R(f)}{\epsilon}\Big)\Big]\Big) + 1 \tag{5.2.18}$$

steps, and its result $\widehat x$ satisfies

$$\widehat x \in X \quad\text{and}\quad f(\widehat x) - \min_X f \le \epsilon. \tag{5.2.19}$$

Milestones

• Statement (∗), case $n > 1$ (p. 344): the half-ellipsoid $\{x \in E(c,B) \mid a^Tx \le a^Tc\}$ lies in $E(c^+, B^+)$, and $\operatorname{Vol}E(c^+,B^+) = (n/\sqrt{n^2-1})^{n-1}\frac{n}{n+1}\operatorname{Vol}E(c,B) \le e^{-1/(2n)}\operatorname{Vol}E(c,B)$.
• Eq. (5.2.21) (p. 350): $\rho_\tau \le e^{-\tau/(2n^2)}R$ at every step performed.
• Eq. (5.2.28) (p. 352): $L_t \le \operatorname{Var}_R(f)$ for every $t$.
• Claim 2∗ (p. 350): whenever the method terminates, its result is well defined and is a feasible $\epsilon$-solution.

Significance

Theorem 5.2.1 bounds the number of oracle calls by a quantity that depends only on the dimension, on $\ln(R/r)$ and on $\ln(1 + \operatorname{Var}_R(f)/\epsilon)$: the cost of each additional digit of accuracy is $O(n^2)$ steps, whatever the instance. Each step costs one call of each oracle and $O(n^2)$ arithmetic operations. This is the ingredient the book's Theorem 5.3.1 combines with polynomial computability to conclude that convex programs are polynomially solvable, and it is the reason semidefinite and conic quadratic programs, the subject of the earlier lectures, are tractable in theory. The bound is also explicit enough to be checked numerically, with no hidden constants.

On the formal side, the platform has machine-checked versions of related results in other forms: Bertsimas and Tsitsiklis's half-ellipsoid lemma with the weaker ratio $e^{-1/(2(n+1))}$ and polyhedral feasibility version, Bubeck's version for objectives bounded on $X$ with a convergence-rate conclusion, and Shor's localization theorem. None of these is the book's method: its guesses $L_t$, its stopping rule (5.2.17), the explicit step count (5.2.18), or the exact volume identity (5.2.14). A formal proof of Theorem 5.2.1 gives a machine-checked oracle complexity bound with a stopping rule computable from the run alone.

Difficulty

The book's description of the method runs to two pages; the central difficulty is the termination analysis, not the geometry. The volume of the ellipsoids decreases geometrically, but their diameters need not, so the search points $c_t$ need not converge, and the method cannot know how close it is to the optimum. A naive argument that the search points approach the optimum therefore fails, and the stopping test (5.2.17), which only sees $\rho_t$, $r$ and the guesses $L_t$, has to be related to the unknown optimality gap. The analysis must also cover runs in which no step was productive for a long time, and the possibility that the result is undefined. On the geometric side, (∗) requires the exact determinant of a rank-one update and the elementary but not immediate inequality $(n/\sqrt{n^2-1})^{n-1}\frac{n}{n+1} \le e^{-1/(2n)}$. Reasoning about a recursively defined algorithm also means carrying invariants (the ellipsoid contains every point of $X$ not yet cut off, $\operatorname{Det} B_t \ne 0$) through the induction.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and the Euclidean norm eucNorm x = √(x ⬝ᵥ x) is defined explicitly (Mathlib's norm on Fin n → ℝ is the sup norm). Volumes are MeasureTheory.volume on Fin n → ℝ, valued in ℝ≥0∞. The setting (5.2.9) with assumption A is the predicate IsBlackBoxProgram f X r R. The oracles are arbitrary functions of the query point satisfying (5.2.10) and (5.2.11); every theorem is quantified over all of them, and none sees the centre $\bar x$. The method is a function run from the number of steps performed to an outcome, running with the current $c_t, B_t, L_t$ and best productive point, or stopped with an optional result; TerminatesAt t res says the run stops exactly at step $t \ge 1$. $\max_{E_0} f$ and $\min_{E_0} f$ are reals given by IsGreatest/IsLeast, and $\min_X f$ is expressed by comparison with every point of $X$, so no supremum or infimum with a default value occurs. Ceil is Int.ceil and the step bound is compared in $\mathbb Z$. A statement about an arbitrary sequence of ellipsoids or an arbitrary "state" carrying no link to the run would trivialize the goal; here the ellipsoids, guesses and result are those the method constructs from the oracles' answers.

Beyond the paper. The book's statement (∗) also has a case $n = 1$, whose printed centre $c - \frac12 Ba/|Ba|$ moves by $\frac12$ regardless of the segment's length; the containment fails for $c = 0$, $B = 4$, $a = 1$. The case is posed as printed (expected to be disproved) and as a corrected variant with centre $c - \frac12 B\,(Ba/|Ba|)$. Theorem 5.2.1 assumes $n \ge 2$ and is unaffected.

A complete development needs the determinant of a rank-one update (Matrix.det_add_replicateCol_mul_replicateRow), Lebesgue measure of linear images (MeasureTheory.Measure.addHaar_image_linearMap), the continuity of convex functions on $\mathbb R^n$, and an induction over run. The ellipsoid update lemma and the oracle and method definitions are reusable for other cutting-plane methods. Proofs of individual milestones, in particular (∗), are welcome as separate contributions.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, MPS/SIAM Series on Optimization, SIAM, 2001. doi:10.1137/1.9780898718829
• D. B. Yudin, A. S. Nemirovski, Informational complexity and efficient methods for the solution of convex extremal problems, Ekonomika i Matematicheskie Metody 12 (1976), 357–369.
• N. Z. Shor, Cut-off method with space extension in convex programming problems, Cybernetics 13 (1977), 94–96. doi:10.1007/BF01071394
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Math. Doklady 20 (1979), 191–194. mathnet
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. doi:10.1007/978-3-642-97881-4