Optimization

How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.

Matrix completion — recovering a low-rank matrix $M = ZZ^\top$ from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective

where $\Omega=\{(i,j)|M_{i,j} \text{ is observed}\}$ and $R(X)$ is a certain regularizer. from a random starting point, and it just works.

Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has no spurious local minima — every local minimum is global and exactly recovers $M$. This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum $X$ of $f$ satisfies $XX^\top = ZZ^\top$.

Motivation

Chapter 4 of F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) applies the product-form theory of Chapter 3 to concrete systems. Two of its results have numbered statements, and they answer two practical questions.

The first comes from the design of store-and-forward communication networks (telegraph and packet-switched data networks). Messages queue at channels; the designer chooses each channel's capacity subject to a budget, and wants to minimize the delay messages suffer. Because the equilibrium law at every channel is geometric under several different modelling assumptions (§4.1, pp. 95–96), the mean delay has a closed form, and the budget allocation problem becomes a small convex program with an explicit solution. This square-root capacity assignment goes back to L. Kleinrock's work on communication nets (Communication Nets, McGraw-Hill, 1964) and remains the textbook example of optimal design for a network of queues.

The second comes from compartmental models in biology, birth–illness–death processes and manpower planning (§4.5, pp. 113–115). Individuals enter a system as a Poisson stream and move through it independently. Equilibrium results follow from Chapter 3; Theorem 4.2 describes the transient behaviour exactly, starting from an empty system.

Setting

Capacity allocation (§4.1). A network has $J \ge 1$ channels. Channel $j$ receives traffic at average rate $a_j > 0$ and is given capacity $\phi_j$. In equilibrium the number $n_j$ of messages at channel $j$ has the geometric law (4.1),

which requires $\phi_j > a_j$. Its mean is $a_j/(\phi_j - a_j)$. Capacity on channel $j$ costs $f_j > 0$ per unit and the total budget is $F$, giving the cost constraint (4.2)

The mean number of customers in the network is

and the feasible set is the set of $\phi \in \mathbb{R}^J$ with $\phi_j > a_j$ for every $j$ that satisfy (4.2). In Lean these are meanNumberInNetwork a φ and FeasibleCapacities a f F. The proof works with the Lagrangian lagrangian a f F y φ $= N(\phi) + y(\sum_j f_j\phi_j - F)$.

Compartmental model (§4.5). Individuals arrive in a Poisson stream of rate $\nu > 0$ at a system of $J$ compartments that is empty at time $0$. Let $p_j(s)$ be the probability that an individual is in compartment $j$ a time $s$ after its arrival; $p_j(s) \ge 0$ and $\sum_j p_j(s) \le 1$, since individuals may leave. Let $n_j(t)$ be the number of individuals in compartment $j$ at time $t > 0$, and

In Lean the model is the predicate IsCompartmentModel P ν t p M T Loc, the counts are compartmentCount M Loc j, and $\alpha_j(t)$ is alpha p j t.

Formalization targets

Goal: Theorem 4.1 (p. 97)

If $J \ge 1$, $a_j > 0$, $f_j > 0$ and $F > \sum_k a_k f_k$, then

is feasible and minimizes $N$ over the feasible set, and every other feasible $\phi$ has $N(\phi) > N(\phi^*)$.

Milestones toward the goal

1. The mean of the geometric law (4.1) is $a_j/(\phi_j - a_j)$ (p. 97).
2. For $y > 0$ the Lagrangian is minimized over $\{\phi_j > a_j\}$ by $\phi_j = a_j + \sqrt{a_j/(y f_j)}$ (proof of Theorem 4.1).
3. The choice $1/\sqrt y = (F - \sum_k a_k f_k)/\sum_k\sqrt{a_k f_k}$ makes that minimizer equal to $\phi^*$ and feasible for (4.2).

Second result: Theorem 4.2 (pp. 114–115)

The proof's generating-function identity, for $z_j \in [0,1]$,

and the theorem itself: $n_1(t), \dots, n_J(t)$ are independent and $n_j(t)$ is Poisson with mean $\nu\alpha_j(t)$.

Significance

Theorem 4.1 is a closed-form design rule. Every channel first receives the capacity $a_j$ needed to carry its traffic; the remaining budget is shared in proportion to $\sqrt{a_j f_j}$, not to the traffic $a_j$. Sizing capacity in proportion to the load, which is the obvious rule, is therefore not optimal. The same calculation applies to any network whose stations have the geometric law (4.1), for example a manufacturing job shop (p. 97). The mean number in the network and the mean time a customer spends in it are minimized together.

Theorem 4.2 is the exact transient law of a network of infinite-server queues started empty. It holds however complicated the motion of an individual is, provided individuals move independently, and letting $t \to \infty$ it recovers the equilibrium Poisson law of §4.5.

Both results are classical and proved in the book. Neither is formalized on Prove2Me. The platform has the geometric equilibrium law of the M/M/1 queue (KellyStochasticNetworks.mm1_equilibrium) but not its mean, and no result on Poisson thinning or marking by independent random locations. The formal work for Theorem 4.1 is a strict-convexity and Lagrangian-sufficiency argument in $\mathbb{R}^J$. For Theorem 4.2 it is a Poisson marking theorem in measure-theoretic probability. Both pieces are reusable.

Difficulty

For Theorem 4.1, the book's proof sets the partial derivatives of the Lagrangian to zero. A stationary point is not a global minimizer in general, so the formal proof must show that $L$ is (strictly) convex on the open region $\phi_j > a_j$, and it must use Lagrangian sufficiency, not first-order conditions alone. The region is open and the objective is unbounded near its boundary. Feasibility of $\phi^*$ needs $F > \sum_k a_k f_k$, which the book leaves implicit.

For Theorem 4.2, the steps of the proof that read "conditional on $M$" have to be carried out with measure-theoretic independence. One step averages a product over $M$ independent uniform instants. Another sums the Poisson mixture into an exponential. The last turns a factorized generating function into mutual independence of $J$ counts with Poisson marginals. Mathlib has the Poisson distribution (ProbabilityTheory.poissonMeasure) but no marking or thinning theorem, and no uniqueness theorem for multivariate probability generating functions.

Formalization scope

Channels and compartments are indexed by Fin J; all rates, costs and capacities are real numbers.

Theorem 4.1. The statement carries the book's implicit hypotheses explicitly: $J \ge 1$, $a_j > 0$, $f_j > 0$, $F > \sum_k a_k f_k$. Stability $\phi_j > a_j$ is part of the feasible set. The conclusion is global optimality over the feasible set (IsMinOn) together with feasibility of $\phi^*$, plus strict optimality against every other feasible point. Uniqueness is a slight strengthening of the book's "the optimal allocation is", and it holds by strict convexity. A statement that $\phi^*$ satisfies (4.2), or that it is a stationary point of the Lagrangian, is not the theorem: those are one-line computations or the proof method, and the goal is stated as global optimality to rule them out.

Theorem 4.2. The model is pinned down as in the proof on p. 115:

• the number $M$ of arrivals in $(0,t)$ is Poisson with mean $\nu t$;
• an i.i.d. sequence of (arrival instant, location at time $t$) pairs is independent of $M$, and only its first $M$ entries are used;
• each instant is uniform on $(0,t)$, and an individual arriving at $u$ is in compartment $j$ at time $t$ with probability $p_j(t-u)$, or has left.

"Individuals move independently" is formalized as this conditional independence. The $p_j$ are measurable sub-probabilities, not assumed to sum to one. The conclusion is mutual independence of the $J$ counts (iIndepFun) together with the Poisson probability mass function of each. Infinite time horizons and the point-process description of the system are out of scope.

Useful contributions: a reusable Lagrangian-sufficiency lemma for separable convex objectives under one linear constraint; a Poisson marking (colouring) theorem for finitely many colours; the multivariate generating-function uniqueness lemma for $\mathbb{N}^J$-valued random vectors.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979, Chapter 4 (§4.1, pp. 95–97; §4.5, pp. 113–115).
• L. Kleinrock, Communication Nets: Stochastic Message Flow and Delay, McGraw-Hill, 1964 (reprinted Dover, 1972).
• J. F. C. Kingman, Poisson Processes, Oxford University Press, 1993 (colouring and marking theorems).

Motivation

A single machine must process a set of jobs, each with a processing time and a due date, and the cost of a schedule depends on how late the jobs finish. Total tardiness is the classical criterion, but in many applications lateness is penalised more than proportionally: a job one week late costs more than twice a job half a week late, and a quadratic or other convex penalty describes this better. Hamilton Emmons's 1969 paper in Operations Research (DOI 10.1287/opre.17.4.701) derives dominance rules for total tardiness and then asks which of them survive when total tardiness is replaced by $\sum_J g(T_i)$ for an arbitrary convex nondecreasing loss $g$.

Timeline of the relevant results:

• 1955 — Jackson shows that ordering jobs by earliest due date (EDD) minimises the maximum lateness, and hence produces a schedule without late jobs whenever one exists.
• 1956 — Smith gives the ratio rule for weighted completion time and an adjacent-interchange criterion for pairs of jobs.
• 1969 — Emmons proves the precedence theorems for total tardiness that underlie later branch-and-bound and dynamic programming algorithms for $1\,||\,\sum T_j$, and shows (p. 713) that Theorems 2 and 3 and part of Theorem 1 extend to any sum of identical convex nondecreasing tardiness penalties.
• 1977 — Lawler's pseudo-polynomial algorithm for total tardiness builds on Emmons's conditions; the problem is later shown NP-hard (Du and Leung, 1990).

Setting

A finite set $J$ of jobs is to be sequenced on one machine. Job $J_i$ has a processing time $p_i\ge 0$ and a due date $d_i$. All jobs are available at time $0$, and the machine processes them one after another without idle time. A schedule is an ordering $l$ of the jobs of $J$. The completion time $C_i$ of $J_i$ in $l$ is the sum of the processing times of $J_i$ and of every job before it; its waiting (starting) time is $W_i=C_i-p_i$, and its tardiness is

A loss function $g:\mathbb R\to\mathbb R$, convex and nondecreasing on $[0,\infty)$, is fixed, the same for every job. The objective is $\sum_{i\in J} g(T_i)$, and a schedule is optimal if no schedule of $J$ has a smaller objective. With $g(T)=T$ this is total tardiness.

Where the paper uses job indices, the jobs are indexed in SPT order: $j<k$ implies $p_j<p_k$, or $p_j=p_k$ and $d_j\le d_k$. The notation $j\leftarrow k$ means that some optimal schedule has $J_j$ before $J_k$; for a set $A_k$ of jobs, $k\leftarrow A_k$ means that some optimal schedule has $J_k$ before every job of $A_k$, and $A_k'$ is the set of jobs of $J$ not in $A_k$. An EDD schedule sequences the jobs in nondecreasing order of due dates.

Formalization targets

Goal: Corollary 2.2* (p. 713)

If an EDD schedule $l$ of $J$ satisfies

then $l$ minimises $\sum_J g(T_i)$ over all schedules of $J$, for every $g$ convex and nondecreasing on $[0,\infty)$.

The goal fixes no constant and no particular $g$: it is a statement about the whole class of convex nondecreasing penalties.

Milestones (in attack order)

1. Convex exchange condition (p. 713): if $T_{ja}\le T_{jb}$, $T_{kb}\le T_{ka}$ (all nonnegative), $T_{ka}-T_{kb}\le T_{jb}-T_{ja}$ and $T_{jb}\ge T_{ka}$, then $g(T_{ka})-g(T_{kb})\le g(T_{jb})-g(T_{ja})$.
2. Theorem 1* (p. 713): for $j<k$, if $d_j\le d_k$ then $j\leftarrow k$.
3. Theorem 2* (p. 713): for $j<k$, if $k\leftarrow A_k$, $d_j>d_k$ and $d_j+p_j\ge\sum_{A_k'}p_i$, then $k\leftarrow j$.
4. Corollary 2.1* (p. 713): if $d_j=\max_i d_i$ and $d_j+p_j\ge\sum_J p_i$, then some optimal schedule ends with $J_j$.
5. Last-job reduction (proof of Corollary 2.2, p. 706): if some optimal schedule ends with $J_j$, any optimal schedule of $J\setminus\{J_j\}$ followed by $J_j$ is optimal for $J$.

Two further statements of the same section are included as items: Corollary 1.3* (the SPT schedule is optimal if it coincides with the EDD schedule) and Theorem 3 for the generalised objective.

Significance

The goal says that EDD is optimal for every convex nondecreasing tardiness penalty as long as no job starts after its due date. The classical sufficient condition, that at most one job is tardy, follows from Jackson's rule; Emmons's condition allows any or all jobs to be tardy, provided each is tardy by at most its own processing time. Because the conclusion holds for the whole class of penalties at once, an instance satisfying it needs no knowledge of $g$: total tardiness, total squared tardiness, and any other convex nondecreasing cost are minimised by the same sequence. Theorems 1* and 2* are the dominance rules that the paper's ordering procedure applies pairwise; they reduce the search space of branch-and-bound methods for convex tardiness objectives.

The results are proved in the paper (for $\sum g(T_i)$ the proofs are said to be "easily established" and omitted). None of them has, to our knowledge, a machine-checked proof. The mission produces formal statements and proofs of the generalised results, including the omitted ones, on top of a reusable single-machine model.

Difficulty

The total-tardiness proofs compare changes in tardiness additively: an interchange is good if the decrease in one job's tardiness is at least the increase in another's. For a convex $g$ this comparison is not enough, because a unit of tardiness costs more at higher tardiness levels; the changes must also occur at the right height on the curve, and part (b) of the proof of Theorem 1 fails for this reason. Each generalised argument therefore has to check, for every job whose tardiness changes, both the size and the location of the change, including jobs whose tardiness changes from zero to positive. Ties for the latest due date are a further obstacle: the printed proof of Corollary 2.1 cites Theorem 2, whose hypothesis $d_j>d_k$ is strict, so a job sharing the maximum due date is not covered by the argument as written, although the corollary is stated without excluding ties.

Formalization scope

Jobs are elements of a type $\iota$; the job set is a Finset $J$, processing times and due dates are real functions $p,d:\iota\to\mathbb R$. Where the paper's index matters, $\iota$ is linearly ordered and its order is the job index, together with the SPT-indexing hypothesis. A schedule is a duplicate-free list whose elements are exactly $J$, and completion times are the published single-machine definition MooreLateJobs.Shared.completionTime (Moore 1968), which starts the machine at time $0$ with no idle time. Optimality is against every schedule of $J$. The relation $j\leftarrow k$ is formalised as the existence of an optimal schedule with $J_j$ before $J_k$ (keeping the premise $k\leftarrow A_k$ in the conclusion where the theorem has one); the paper's cumulative reading of the notation is not formalised.

Standing assumptions and deviations:

• $g$ is convex and nondecreasing on $[0,\infty)$ only; the page's "increasing" is read as nondecreasing, as in the abstract. No smoothness, strict monotonicity or $g(0)=0$ is assumed.
• Processing times are assumed nonnegative; this is added (they are durations).
• The reduction $d_i<\sum_J p_i$ of p. 703 is not assumed, which makes the statements apply to more instances.
• "The EDD schedule" is any schedule with nondecreasing due dates; ties are arbitrary.

A trivializing formalization is ruled out: the goal requires optimality of the given EDD list against every schedule of $J$, not of some EDD list, and a sorry-free check shows its hypotheses hold on a two-job instance in which both jobs are tardy.

A complete development needs list lemmas for moving one job to a later position, the effect of such moves on completion times, and slope inequalities for convex functions on $[0,\infty)$. The schedule-manipulation lemmas are reusable for other single-machine sequencing results. Proofs of any milestone, of the two further items, and of general interchange lemmas are welcome.

Selected references

• H. Emmons, One-Machine Sequencing to Minimize Certain Functions of Job Tardiness, Operations Research 17(4):701–715, 1969. https://doi.org/10.1287/opre.17.4.701
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3:59–66, 1956. https://doi.org/10.1002/nav.3800030106
• E. L. Lawler, A "Pseudopolynomial" Algorithm for Sequencing Jobs to Minimize Total Tardiness, Annals of Discrete Mathematics 1:331–342, 1977. https://doi.org/10.1016/S0167-5060(08)70742-8
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. Du and J. Y.-T. Leung, Minimizing Total Tardiness on One Machine is NP-Hard, Mathematics of Operations Research 15(3):483–495, 1990. https://doi.org/10.1287/moor.15.3.483

Motivation

The gradient method minimizes a differentiable function $f$ on $\mathbb{R}^n$ by moving from the current point $x_k$ along the negative gradient, $x_{k+1} = x_k - \lambda_k \nabla f(x_k)$. Every practical implementation has to choose the step $\lambda_k$. A fixed step requires knowing a Lipschitz constant of $\nabla f$; an exact line search is expensive. Larry Armijo's four-page note (Pacific J. Math. 16 (1966) 1–3) proved that any step achieving a sufficient decrease proportional to $|\nabla f(x_k)|^2$ yields convergence, and gave the halving rule that is now called the Armijo rule or backtracking line search. The rule is the default step-size strategy of gradient, quasi-Newton and Newton-type methods in textbooks such as Nocedal–Wright and Bertsekas, and its sufficient-decrease test reappears in essentially every later line-search analysis.

Timeline:

• 1944, H. B. Curry: convergence of steepest descent when each step minimizes $f$ along the ray, which needs a one-dimensional minimization per step (Quart. Appl. Math. 2).
• 1962, A. A. Goldstein: convergence of the gradient method with a rate estimate, assuming $f \in C^2$ on a bounded level set $S(x_0)$ and a known bound on the Hessian norm there (Numer. Math. 4).
• 1966, L. Armijo (received January 1964): the convergence theorem below for any step with sufficient decrease $\delta|\nabla f(x_k)|^2$, $0 < \delta \le 1/(4K)$, under a Lipschitz condition on $\nabla f$ restricted to the level set, with the fixed-step and halving-step algorithms as corollaries. The paper's §3 places these hypotheses between Curry's (weaker) and Goldstein's (stronger).

Setting

Let $E^n$ be real Euclidean $n$-space with norm $|\cdot|$, and let $f : E^n \to \mathbb{R}$ be continuous and bounded below. For a fixed $x_0 \in E^n$ the level set is $S(x_0) = \{x : f(x) \le f(x_0)\}$. Write $\nabla f(x)$ for the gradient of $f$ at $x$. "$f \in C^1$ on $S(x_0)$" means that $f$ is differentiable at every point of $S(x_0)$ and $\nabla f$ is continuous there.

• Condition III at $x_0$: $f \in C^1$ on $S(x_0)$ and there is a Lipschitz constant $K > 0$ with $|\nabla f(y) - \nabla f(x)| \le K|y - x|$ for all $x, y \in S(x_0)$.
• Condition IV at $x_0$: $f \in C^1$ on $S(x_0)$, $x^*$ is a point with $f(x^*) = \inf_{E^n} f$, and for every $r > 0$

with $m(r) = \infty$ when the set is empty. Condition IV forces $x^*$ to be the unique minimizer and the only stationary point in $S(x_0)$.

For $\delta > 0$ and $x \in S(x_0)$, the sufficient-decrease set of display (1) is

The steepest descent algorithm uses $x_{k+1} = x_k - \frac{1}{2K}\nabla f(x_k)$. The modified steepest descent algorithm fixes $\alpha > 0$, sets $\alpha_m = \alpha/2^{m-1}$, and takes $x_{k+1} = x_k - \alpha_{m_k}\nabla f(x_k)$ with $m_k$ the smallest positive integer such that

Formalization targets

Goal: the convergence theorem (§2, pp. 1–2)

Assume $f$ is continuous and bounded below and Conditions III and IV hold at $x_0$. If $0 < \delta \le 1/(4K)$, then for every $x \in S(x_0)$

and every sequence with first term $x_0$ and $x_{k+1} \in S^*(x_k,\delta)$ for all $k$ satisfies

Milestones (the claims of the proof, p. 2)

1. Along such a sequence, $|\nabla f(x_k)| \to 0$.
2. Under Condition IV, a sequence in $S(x_0)$ with $|\nabla f| \to 0$ converges to $x^*$.

Further claims of the proof (p. 2)

• For $x \in S(x_0)$ and $0 \le \lambda \le 1/K$: $f(x_\lambda) - f(x) \le -(\lambda - \lambda^2K)|\nabla f(x)|^2$.
• $x_\lambda \in S^*(x,\delta)$ for $\lambda_1 \le \lambda \le \lambda_2$, $\lambda_i = \frac{1}{2K}[1 + (-1)^i\sqrt{1 - 4\delta K}]$.
• Along such a sequence, $x_k \in S(x_0)$ and $f(x_k)$ is nonincreasing.

Companion results

• Corollary 1: the steepest descent iterates converge to $x^*$.
• Corollary 2: the modified steepest descent iterates converge to $x^*$, for every $\alpha > 0$.
• The index $m_k$ of Corollary 2 exists; $m_k = 1$ if $\alpha \le 1/(2K)$ and $\alpha_{m_k} > 1/(4K)$ otherwise; the half-step estimate $f(x_\lambda) - f(x) \le -\frac12\lambda|\nabla f(x)|^2$ for $0 \le \lambda \le 1/(2K)$.
• The §1 remark: Condition IV implies Conditions I and II, and is equivalent to them when $S(x_0)$ is bounded.

Significance

The theorem separates the analysis of a gradient method from the choice of its step: whatever rule produces steps in $S^*(x_k, \delta)$ converges, and the two corollaries show that both a fixed step $1/(2K)$ and a halving search started from an arbitrary $\alpha$ qualify. The halving rule needs no knowledge of $K$, which is why it became the standard globalization device for descent methods. The hypotheses are local to the level set: $\nabla f$ need only be Lipschitz on $S(x_0)$, not on all of $E^n$, so functions whose gradient is only locally Lipschitz, such as polynomials of degree above two with bounded level sets, satisfy Condition III.

The result is classical and proved on the page; it has not, to our knowledge, been machine-checked in this form. Formalizing it provides a verified sufficient-decrease convergence theorem with level-set-local hypotheses, a verified Armijo backtracking rule with explicit constants $\tfrac12$, $1/(4K)$ and $1/(8K)$, and reusable definitions (sufficient-decrease set, Armijo test with halving steps) on which later line-search results can build.

Difficulty

The mean value step in the proof of the descent inequality silently uses the Lipschitz bound along the whole segment from $x$ to $x - \lambda\nabla f(x)$, but Condition III gives it only on $S(x_0)$. One has to show that the segment cannot leave the closed set $S(x_0)$ for $0 \le \lambda \le 1/K$; replacing the hypothesis by a global Lipschitz condition is not acceptable, because it changes the theorem. The final step needs Condition IV in its exact form: gradients tending to zero along the iterates do not by themselves give convergence of the iterates, and the positive lower bound $m(r)$ away from $x^*$ is what turns stationarity into convergence. Corollary 2 additionally requires a termination argument for the halving search and a uniform lower bound on accepted steps.

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), $|\cdot|$ is the norm and $\nabla f$ is Mathlib's gradient f. All declarations live in the namespace ArmijoGrad.Conv, with one definition file ArmijoGrad.Conv.Setting.

Committed conventions:

• The standing assumptions of §2 are binders of the goal and the corollaries: Continuous f, BddBelow (Set.range f), ConditionIII f x0 K, ConditionIV f x0 xstar. Milestones keep only the assumptions their claim uses, which makes them more general; nothing is added.
• "$f \in C^1$ on $S(x_0)$" is differentiability at every point of $S(x_0)$ plus continuity of gradient f on $S(x_0)$. The Lipschitz bound of Condition III holds on $S(x_0)$ only; $K > 0$ is part of Condition III.
• Condition IV carries its minimizer $x^*$ and states $m(r) > 0$ as the existence of a positive lower bound for $|\nabla f|$ on $\{x \in S(x_0) : |x - x^*| \ge r\}$; this matches the convention $m(r) = \infty$ on the empty set. No real infimum is used.
• Sequences are ℕ → EuclideanSpace ℝ (Fin n) with first term equal to $x_0$, the base point of $S(x_0)$, as in the paper's notation.
• $\lambda > 0$ in (1) is strict. $\alpha_m = \alpha/2^{m-1}$ is used only with $m \ge 1$, and $m_k$ is required to be the smallest such index.

A trivializing formalization is ruled out: the goal assumes nothing about $\lambda_1, \lambda_2$, the descent inequality or $|\nabla f(x_k)| \to 0$, Condition IV cannot hold vacuously because it names a minimizer, and all hypotheses are satisfiable by nontrivial data: $f(x) = |x|^2/2$ satisfies Conditions III and IV with $K = 1$ and $x^* = 0$, and both algorithms have runs for it.

A complete development needs the one-dimensional mean value inequality along a segment, a continuity argument keeping the segment in $S(x_0)$, the telescoping bound for monotone sequences bounded below, and the halving-search termination. The definitions file and the descent and Armijo-index lemmas are reusable for later line-search missions. Contributions are welcome on every milestone; the descent inequality is the natural first target.

Selected references

• L. Armijo, Minimization of functions having Lipschitz continuous first partial derivatives, Pacific Journal of Mathematics 16(1), 1–3, 1966. https://doi.org/10.2140/pjm.1966.16.1
• H. B. Curry, The method of steepest descent for non-linear minimization problems, Quarterly of Applied Mathematics 2, 1944. https://doi.org/10.1090/qam/10667
• A. A. Goldstein, Cauchy's method of minimization, Numerische Mathematik 4, 146–150, 1962. https://doi.org/10.1007/BF01386306
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-0-387-40065-5

Motivation

The question behind this mission was posed by T. E. Harris to L. R. Ford, Jr. and D. R. Fulkerson at RAND, in the setting of rail transport: given a rail network linking two cities, with a capacity on every link, find the largest steady flow from one city to the other. Ford and Fulkerson's answer, the minimal cut theorem, published in the Canadian Journal of Mathematics in 1956 (DOI 10.4153/CJM-1956-045-5), says that the obvious upper bound, the total capacity of a set of links whose removal separates the two cities, is always achieved by some flow.

The theorem became the starting point of network flow theory, and through it of a large part of combinatorial optimization and operations research: transportation, assignment, scheduling and network reliability problems are routinely reduced to it.

Timeline.

• 1927: K. Menger proves that the minimum number of vertices separating two vertex sets of a graph equals the maximum number of disjoint paths joining them (Fund. Math. 10), the unit-capacity ancestor of the theorem.
• 1955: Harris and Ross study the Soviet rail network as a capacity problem in a RAND report; Harris formulates the maximal flow problem (Schrijver's historical account: Math. Program. 91, 2002).
• 1956: Ford and Fulkerson publish the minimal cut theorem for undirected networks, with a non-constructive proof based on maximal flows (this paper). Independently, Elias, Feinstein and Shannon state and prove the max-flow min-cut theorem for directed networks (IRE Trans. Inf. Theory 2, 1956), and Dantzig and Fulkerson obtain it from linear programming duality.
• 1956–1962: Ford and Fulkerson's labelling (augmenting path) algorithm, collected in Flows in Networks (Princeton, 1962).
• 1972: Edmonds and Karp give polynomial bounds for augmenting-path methods (J. ACM 19).

Setting

A network $N$ consists of a finite set of vertices $V$, a finite set of arcs $E$, two distinct vertices, the source $a$ and the sink $b$, and a positive capacity $c(e)>0$ on every arc. Each arc $e$ has two distinct end vertices; arcs are undirected, and several arcs may join the same pair of vertices.

A chain joining $u$ and $w$ is a set of distinct arcs that can be arranged as $\alpha_1(v_0v_1),\alpha_2(v_1v_2),\dots,\alpha_m(v_{m-1}v_m)$ with $v_0=u$, $v_m=w$ and the vertices $v_0,\dots,v_m$ pairwise distinct; each arc may be traversed in either direction. The null chain ($m=0$) joins $u$ to itself.

A flow $f$ assigns a number $f(C)\ge 0$ to each chain $C$ joining $a$ and $b$ (and $0$ to every other set of arcs) such that the load $\ell_f(e)=\sum_{C\ni e}f(C)$ satisfies $\ell_f(e)\le c(e)$ for every arc. Its value is $\mathrm{val}(f)=\sum_C f(C)$. An arc is saturated by $f$ if $\ell_f(e)=c(e)$. A maximal flow is a flow of largest value.

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$; its value is $v(D)=\sum_{e\in D}c(e)$. A cut is a disconnecting set no proper subset of which is disconnecting.

The proof introduces two further objects: the set $S$ of arcs saturated by every maximal flow, and the set $L\subseteq S$ of left arcs, those arcs of $S$ whose left vertex (the end vertex met first by a positive chain flow of a maximal flow, travelling from $a$) can be reached from $a$ by a chain with no arc saturated by some maximal flow.

Formalization targets

Goal: Theorem 1 (Minimal cut theorem), p. 400

with both the maximum and the minimum attained. The statement mentions only flows and disconnecting sets, not the proof objects $S$ and $L$.

Milestones, in the order of the paper's proof

1. A maximal flow exists, and the set of maximal flows is convex (p. 400).
2. Lemma 1: $S$ is a disconnecting set (p. 400).
3. Every arc of $S$ receives the same orientation from all positive chain flows of all maximal flows: its left vertex is unique (pp. 400–401).
4. Lemma 2: $L$ is a disconnecting set (p. 401).
5. Lemma 3: no positive chain flow of a maximal flow contains more than one arc of $L$ (p. 401).
6. $\mathrm{val}(f)\le v(D)$ for every flow $f$ and every disconnecting set $D$ (p. 402).
7. $L$ is a cut of minimal value, and every maximal flow has value $v(L)$ (p. 402).

Two further statements of the paper are included as items without being milestones: the remark that a disconnecting set of minimal value is a cut (p. 400), and the Corollary (p. 402): if a set $A$ of arcs meets every cut in exactly one arc, adding $k$ to the capacity of each arc of $A$ raises the maximal flow value by $k$.

Significance

The minimal cut theorem turns a maximization over flows into a minimization over finite sets of arcs, so an optimal flow comes with a short certificate of optimality. It implies Menger's theorem (unit capacities), and through it König's theorem on bipartite matchings and Hall's marriage theorem. The Corollary is the tool behind the paper's own computing procedure for source–sink planar networks (§2, formalized in a companion mission).

The theorem is classical and proved. What this mission adds is a machine-checked proof of the paper's own formulation: undirected arcs, parallel arcs, flows decomposed along chains (path flows, with no circulations), and the minimum taken over arc sets meeting every chain, together with the proof's intermediate claims. Max-flow min-cut theorems already on the platform (Applied Combinatorics VIII, AppliedComb.Flows.max_flow_min_cut; Introduction to Linear Optimization X, LinearOptimization.max_flow_min_cut) concern directed networks with edge flows obeying conservation and cuts given by vertex sets. They are related results, not this statement, and connecting the two models is itself welcome work.

Difficulty

Weak duality (milestone 6) is immediate; the content is the reverse inequality. The obvious first step, taking a maximal flow and observing that its saturated arcs separate $a$ from $b$, does not finish the proof: a positive chain flow may pass through several saturated arcs, so the total capacity of the saturated arcs can exceed the flow value. One has to single out a disconnecting subset that every positive chain flow crosses exactly once, and there is no canonical choice from a single flow. The paper's sets $S$ and $L$ are defined from all maximal flows at once, and the work consists in showing that these sets are well behaved. The orientation claim in particular needs an exchange argument on two chains that cross at an arc, where the recombined arc sequences may revisit vertices and must be reduced to chains. In a formal development this "a walk contains a chain" step and the averaging of maximal flows over finitely many chains are the main bookkeeping costs.

Formalization scope

• A network is a structure on a vertex type V and an arc type E, both Fintype with decidable equality, with end-vertex maps tail, head (labels only, no direction), tail e ≠ head e, a source and a sink with source ≠ sink, and capacities cap : E → ℝ with 0 < cap e. These are the paper's standing assumptions; there are no others in §1. In particular, no planarity is assumed and an arc may join $a$ and $b$ directly.
• A chain is a Finset E that is the arc set of some arrangement (list of arcs, list of pairwise distinct vertices, each arc joining consecutive vertices in either order).
• A flow is a function f : Finset E → ℝ, non-negative, zero off the chains joining source and sink, with every arc load at most the capacity. A collection of chain flows that lists a chain twice merges into this form without changing the value or any load.
• "Maximal" means of maximum value. The goal is stated with IsGreatest and IsLeast on the sets of flow values and of values of disconnecting sets, so no supremum of a real set appears and both extrema must be attained.
• A trivializing formalization is ruled out: chains must be self-avoiding and must join the source and the sink, the disconnecting condition quantifies over exactly these chains, and the minimum ranges over all disconnecting sets rather than over a family chosen to match a given flow.
• Needed infrastructure: finite sums over Finset (Finset E), convexity in Finset E → ℝ, compactness of the flow polytope (for existence), and lemmas on lists (extracting a chain from a walk). The walk-to-chain lemma and weak duality are reusable for the companion mission and for any path-flow model.

Selected references

• 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
• K. Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115
• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• J. Edmonds and R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19 (1972), 248–264. https://doi.org/10.1145/321694.321699
• A. Schrijver, On the history of the transportation and maximum flow problems, Mathematical Programming 91 (2002), 437–445. https://doi.org/10.1007/s101070100259