All missions

Motivation

The single-machine sequencing problem with precedence constraints, written $1\mid\mathrm{prec}\mid\sum w_jC_j$, asks for an order of $n$ jobs on one machine that respects a given acyclic digraph of precedences and minimizes the weighted sum of completion times. It is NP-hard in general (Lawler 1978; Lenstra and Rinnooy Kan 1978), and much of its structural theory goes through a decomposition due to Sidney (Sidney 1975): find an initial set of jobs of maximum weight-to-processing-time ratio, schedule it first, and recurse on the rest. Sidney's decomposition underlies the series-parallel algorithm of the same report, the 2-approximation algorithms for the general problem, and the vertex-cover view of Chudak–Hochbaum, Correa–Schulz and Ambühl–Mastrolilli.

The decomposition is only usable if a ratio-maximal initial set can be found efficiently. Section 7 of E. L. Lawler's report Sequencing jobs to minimize total weighted completion time subject to precedence constraints (IRIA-LABORIA Rapport de Recherche No. 205, December 1976; journal version in Annals of Discrete Mathematics 2, 1978) gives the polynomial algorithm: a binary search on the ratio, where each trial value is tested by one minimum-cut computation in an auxiliary network. This mission formalizes the correctness of that procedure.

Timeline.

• 1970: Rhys (Management Science 17) solves the selection problem, the bipartite case of a maximum-weight closed set, by minimum cut.
• 1975: Sidney introduces the decomposition into ratio-maximal initial sets.
• 1976: Lawler (this report) reduces the search for a ratio-maximal initial set to $O(\log n + \log w^* + \log p^*)$ minimum-cut computations.
• 1976: Picard (Management Science 22) treats the maximal closure of a general graph by the same network.

Setting

A finite set $N$ of $n=|N|$ jobs carries an acyclic digraph $G=(N,A)$; job $i$ must precede job $j$ when $G$ has a directed path from $i$ to $j$. Job $j$ has an integer processing time $p_j\ge1$ and an integer weight $w_j$ of either sign.

An initial set of $N$ is a set $I\subseteq N$ that contains, with each of its jobs, every predecessor of that job. The ratio of a nonempty set is

$$\rho(I)=\frac{\sum_{j\in I}w_j}{\sum_{j\in I}p_j},$$

and a nonempty initial set $I^*$ is ρ-maximal if $\rho(I^*)\ge\rho(I)$ for every nonempty initial set $I$. Its ratio $\rho^*$ is the optimal ratio.

For a trial value $\rho$, the trial weights are $\bar w_j=w_j-\rho p_j$. A maximum-weight initial set for $\bar w$ is computed in the network $G^*$: add a source $s$ and a sink $t$, give the arc $(s,j)$ capacity $\max(0,-w_j)$, the arc $(j,t)$ capacity $\max(0,w_j)$, and every arc of $G$ capacity $+\infty$. An $(s,t)$ cutset is a partition $(S,T)$ of the nodes with $s\in S$, $t\in T$, of capacity $c(S,T)=\sum_{i\in S}\sum_{j\in T}c_{ij}$.

The integer data satisfy $-w^*\le w_j\le w^*$ and $1\le p_j\le p^*$, and $\varepsilon=1/(np^*)^2$.

Formalization targets

Goal: the last step of the binary search

If $\rho\le\rho^*\le\rho+\varepsilon$, then every nonempty initial set $I$ of maximum trial weight,

$$\sum_{j\in I'}(w_j-\rho p_j)\le\sum_{j\in I}(w_j-\rho p_j)\quad\text{for all initial sets } I',$$

is ρ-maximal. This is the paper's sentence "At this point the smallest value in the interval is chosen for a trial value ρ. … In either case, the maximum weight initial set I which is determined is ρ-maximal" (pp. 16–17).

Milestones

1. Finite-capacity cutsets of $G^*$ correspond to initial sets $I=T-\{t\}$ (p. 14).
2. A finite cutset has capacity $\sum_{j\in N}\max(0,w_j)-\sum_{j\in I}w_j$ (p. 15).
3. A minimum cutset yields a maximum-weight initial set (p. 15).
4. Cases 1–3: a maximum-weight set of positive, negative or zero trial weight shows that $\rho$ is too small, too large, or optimal (pp. 15–16).
5. Every attainable ratio lies in $[-w^*,w^*]$ (p. 16).
6. Two distinct attainable ratios differ by at least $1/(np^*)^2$ (p. 16).

Significance

The goal is what makes Sidney's decomposition algorithmic: a ρ-maximal initial set can be found by a polynomial number of minimum-cut computations, with the bound $2\log_2 n+\log_2 w^*+2\log_2 p^*+1$ on the number of trial values. Ratio-maximal initial sets are the first step of every Sidney-decomposition-based algorithm for $1\mid\mathrm{prec}\mid\sum w_jC_j$, and the cut network is the standard reduction of maximum-weight closure to minimum cut, used across open-pit mining, project selection and parametric optimization.

The results are classical and proved in the report. No machine-checked version of the closure–cut correspondence, the ratio-separation bound, or the binary-search correctness is known to exist in Lean or on Prove2Me. The mission produces a reusable formal account of initial sets, the network $G^*$ with infinite capacities, and the parametric test of a ratio.

Difficulty

Each step is short on paper; the difficulty is in the corners the paper does not discuss. The paper's "maximum weight initial set" ranges over all initial sets, and the empty set has weight $0$. At $\rho=\rho^*$ the empty set is a maximizer and is not ρ-maximal, so the final step needs a nonempty maximizer; and Case 2, read literally over all initial sets, can never occur. The argument at the left end of the interval also needs the separation bound in the right direction: the printed display ends with "$<$", while the argument needs "$\ge$". Finally, initial sets are closed under predecessors along paths, while a cut only sees single arcs, so the correspondence between finite cuts and initial sets needs the arcs of $G$ to stay inside $N$.

Formalization scope

Jobs are a Finset N in a type ι; the precedence digraph is a relation G with every arc inside N and no directed cycle, and "must precede" is Relation.TransGen G. Weights and processing times are real in the general statements and integers cast to reals in the integer-data statements. Lean evaluates $\rho(\emptyset)=0/0$ as $0$; ρ-maximality and every statement about attainable ratios therefore range over nonempty sets. Capacities take values in WithTop ℝ, with $+\infty=\top$; a pair of nodes that is not an arc of $G^*$ has capacity $0$, and an infinite cut has capacity $\top$. A cutset is given by its sink side $T\subseteq\{s,t\}\cup N$.

Added hypotheses and corrected slips, all disclosed in the items:

• the goal assumes the maximum-weight initial set $I$ is nonempty (the empty-set corner above);
• Cases 2 and 3 maximize over nonempty initial sets;
• the separation bound is stated with $\ge$, against the printed "$<$";
• the capacity display's first line, printed $\sum_{j\in S}c_{sj}$, is read as $\sum_{j\in T}c_{sj}$, as its second line shows;
• the interval $[-w^*,w^*]$ and the separation bound are stated for every nonempty subset of $N$, a slight generalisation.

A trivializing formalization is ruled out: the goal assumes neither Case 1 nor Case 3, nor the separation bound, nor anything about cuts; those appear only as milestones. The running-time statements of §7 and the binary search loop itself are out of scope.

A complete development needs finite sums over finsets, path closure of initial sets, and extended-real arithmetic in WithTop ℝ. The cut network with infinite capacities and the closure correspondence are reusable for any maximum-weight closure problem. Proofs of the milestones, and of the goal from Cases 1 and 3 with the separation bound, are welcome.

Selected references

• E. L. Lawler, Sequencing jobs to minimize total weighted completion time subject to precedence constraints, IRIA-LABORIA Rapport de Recherche No. 205, 1976. https://hal.science/hal-04716371v1 ; journal version Annals of Discrete Mathematics 2 (1978) 75–90, https://doi.org/10.1016/S0167-5060(08)70323-6
• J. B. Sidney, Decomposition algorithms for single-machine sequencing with precedence relations and deferral costs, Operations Research 23 (1975) 283–298. https://doi.org/10.1287/opre.23.2.283
• J. M. W. Rhys, A selection problem of shared fixed costs and network flows, Management Science 17 (1970) 200–207. https://doi.org/10.1287/mnsc.17.3.200
• J.-C. Picard, Maximal closure of a graph and applications to combinatorial problems, Management Science 22 (1976) 1268–1272. https://doi.org/10.1287/mnsc.22.11.1268

Motivation

A flexible manufacturing system processes several part types on shared machines, and a machine that switches from one part type to another pays a set-up time. Real-time, distributed scheduling rules for such systems decide locally, at each machine, when to switch and to which buffer. The simplest such rules are clearing policies: a machine keeps working on its current buffer until that buffer is empty, then switches. Perkins and Kumar (IEEE TAC 34, 1989; reference [18] of Kumar–Seidman 1990) showed that every clear-a-fraction (CAF) policy, a clearing policy that always switches to a buffer holding at least a fixed fraction of the machine's work, keeps all buffers bounded in every acyclic system whenever each machine's load is below one.

Kumar and Seidman (IEEE TAC 1990) showed that acyclicity cannot simply be dropped. In §III of the paper, a two-machine re-entrant line and a two-part-type system, both with every machine loaded below capacity, have clearing trajectories whose buffer levels grow without bound. This mission formalizes the paper's positive result for non-acyclic systems: Theorem 1, a stronger capacity condition under which every CAF policy is stable from every initial state.

Setting

There are $P$ part types and $M$ machines. Part type $p$ enters at rate $d_p>0$ and visits the machines $\mu_{p,1},\dots,\mu_{p,n_p}$ in turn; revisits are allowed. At its $i$-th stage a part waits in buffer $b_{p,i}$ and needs processing time $\tau_{p,i}>0$. Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$, and switching from $b$ to $b'\in B_m$ costs $\delta_{b,b'}\ge0$. Flows are fluid. The level $x_b(t)\ge0$ satisfies $x_b(t)=x_b(0)+u_b(t)-y_b(t)$, where $y_b$ is the cumulative output and $u_b$ the cumulative input: $d_p t$ for the first buffer of a route, the output of the previous buffer otherwise. Each machine works through runs. A run is a set-up for a buffer, during which nothing is processed, followed by processing of that buffer at rate at most $1/\tau_b$, and at exactly that rate while the buffer is nonempty.

A trajectory is clearing (Definition 1) if each machine leaves its buffer exactly at the first time the buffer is empty while another of its buffers is nonempty, and then sets up for such a buffer. It is CAF with constants $\varepsilon_m>0$, $K_m$ (Definition 2) if every set-up commenced at time $t$ is for a buffer with

$$x_{p,i}(t)\ \ge\ \varepsilon_m\sum_{(q,j):\,\mu_{q,j}=m}x_{q,j}(t)-K_m .$$

A trajectory is stable if $\sup_{t\ge0}x_{p,i}(t)<\infty$ for every buffer.

The graph on machines has an arc $m\to m'$ when $m\ne m'$ and some part type visits $m'$ right after $m$. Machines are diconnected, $m\leftrightarrow m'$, when each is reachable from the other. For each buffer, $\lambda_{p,i}$ is the last earlier stage at a different machine, if any, and $\pi_{p,i}$ is that stage's machine, the prior machine. The modified input rate is $d'_{p,i}=1/\tau_{p,\lambda_{p,i}}$ if $\pi_{p,i}\leftrightarrow\mu_{p,i}$, and $d'_{p,i}=d_p$ otherwise (11)–(13).

Formalization targets

Goal: Theorem 1 (p. 294)

If

$$\rho'_m:=\sum_{(p,i):\,\mu_{p,i}=m}d'_{p,i}\,\tau_{p,i}<1\qquad\text{for all } m, \tag{14}$$

then for all $\varepsilon>0$, all $K$, every CAF trajectory from every initial state is stable. The bound on each buffer may depend on the trajectory.

Milestones (the proof's own steps, p. 295)

For a machine $m$ in a minimal class, $V_m(t)=\sum_{\mu_{p,i}=m}x_{p,i}(t)[\tau_{p,i}+\dots+\tau_{p,i+\eta_{p,i}-1}]$ is the work at $m$ (15), and $T_n, T_{n+1}$ are consecutive set-up commencements:

1. (18): $V_m(T_{n+1})\le\max[0,V_m(T_n)-(1-\rho'_m)(T_{n+1}-T_n)+\bar\delta]$.
2. (20): $x_{p^*_n,i^*_n}(T_n)\ge 2\bar\delta/((1-\rho'_m)\tau_{p^*_n,i^*_n})\Rightarrow T_{n+1}-T_n\ge2\bar\delta/(1-\rho'_m)$.
3. $V_m(T_n)\ge\Gamma_m\Rightarrow V_m(T_{n+1})\le V_m(T_n)-\bar\delta$, with the explicit $\Gamma_m$ of p. 295.
4. Every buffer of every machine in a minimal class is bounded.
5. The induction step: with upstream classes bounded, $V_m(T_{n+1})\le\max\{\bar\Gamma,V_m(T_n)-(1-\rho'_m)(T_{n+1}-T_n)+\bar\delta+\bar\Gamma\}$.

Significance

The result. Theorem 1 is a sufficient condition for stability that holds for every system topology and every CAF policy, with no restriction to acyclic flows. It separates two kinds of upstream supply. A machine that is not in a common cycle with its supplier needs capacity only for the average rate $d_p$. A machine that is in such a cycle must budget for the supplier's peak rate. The paper's examples show that some strengthening of $\rho_m<1$ is needed for clearing policies on cyclic systems: they are unstable under $\rho_m<1$ alone. Section V of the paper builds on this gap, with a supervisory mechanism that restores stability under $\rho_m<1$ alone.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. A formalization must turn a two-page argument with a set-up/processing run structure, a starvation case analysis and an induction over the condensation of a directed graph into rigorous statements. The result is a reusable fluid model of scheduling with set-up times. It also makes explicit the conventions of the clearing rule, which the paper leaves informal.

Difficulty

A natural first attempt bounds the total work $V_m$ at each machine separately, using only the average arrival rates. This fails on cyclic systems. A machine downstream in a cycle can receive parts in bursts at the upstream machine's full processing rate $1/\tau$, far above $d_p$; Example 1 of the paper builds exactly such a positive feedback. The proof therefore has to (a) bound the inflow into a machine of a minimal class by the peak rates in (14); (b) handle starvation inside a run, where the machine works below its maximal rate; (c) control the set-up overhead, which the CAF rule amortizes by forcing long runs once $V_m$ is large; and (d) push boundedness down the partial order of classes, where the bounded upstream buffers enter as an additive constant $\bar\Gamma$. Step (d) needs a bound on the total content upstream, not one per buffer.

Formalization scope

• Model. System P M holds the data. Part types, machines and stages are 0-based (paper stage $i$ is Lean stage $i-1$). Trajectory S holds levels, cumulative outputs and runs, with N m : ℕ∞ runs per machine. Time is real, with explicit $t\ge0$. Run starts are nondecreasing and, if infinitely many, tend to infinity. Machines never idle outside runs: idling on an empty buffer is processing at the inflow rate.
• Processing law. The output is bounded by $1/\tau_b$ times the Lebesgue measure of the time spent processing $b$, with equality on intervals of processing of a nonempty buffer.
• Clearing. "Nonempty" in Definition 1 for the buffer switched to is read as nonempty or with inflow starting now. Under this reading the paper's example trajectories are clearing trajectories; read literally, "the first time" would not exist. The emptiness test on the current buffer is literal. The no-early-exit condition holds on the open processing interval.
• Set-ups. Set-ups occur only between distinct buffers. $\bar\delta$ is the largest set-up time between distinct buffers of $m$, or $0$ if there are none. Zero set-up times are allowed; $\bar\delta>0$ is not assumed.
• Constants. $\Gamma_m$, $\bar\tau$, $\underline\tau$, $\bar\Gamma$ are explicit definitions, never existentials. Every denominator is positive under the hypotheses.
• Trivializations ruled out. The trajectory class is not empty: a sorry-free witness (one machine, one buffer, $d\tau<1$, any initial level) satisfies every predicate, together with (14). The goal quantifies over every system, every $\varepsilon>0$ and $K$, and every CAF trajectory. It does not fix a selection rule, an acyclic topology, routes without revisits or positive set-ups.
• Infrastructure. Continuity of the levels (from the rate cap), restarting a trajectory at a run start, inflow bounds via conservation along routes, and the condensation of the machine graph. These are reusable for the related Kumar–Seidman missions on instability and supervisory stabilization. Proofs of the milestones in any order are welcome.

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Transactions on Automatic Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Transactions on Automatic Control 34, 139–148, February 1989 (cited as [18] in Kumar–Seidman 1990; the CAF stability result for acyclic systems).

Motivation

Many graph problems in routing, VLSI layout and scheduling ask for a cut that separates a lot of demand while cutting little capacity. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest flow equals the smallest cut. For several commodities sharing one network this equality fails, and the question becomes how far apart the two quantities can be. Leighton and Rao (J. ACM 46 (1999), extending their FOCS 1988 paper) proved that for uniform demands the gap is at most logarithmic in the number of nodes, and turned the proof into approximation algorithms for a range of NP-hard cut problems.

Their §2.4 extends the result to directed networks, where every edge carries flow in one direction only. The directed version is the one behind their approximation algorithms for directed problems, most prominently the minimum feedback arc set problem (§3 of the paper), where the cut structure of a digraph, not of its underlying undirected graph, is what matters.

Timeline. Ford and Fulkerson (1956): max-flow = min-cut for one commodity. Hu (1963): equality for two commodities in undirected graphs. Shahrokhi and Matula (1990, circulated 1986): the uniform concurrent flow problem and its LP dual. Leighton and Rao (FOCS 1988; J. ACM 1999): $\Omega(\mathcal S/\log n)\le f\le\mathcal S$ for uniform and product demands, undirected and directed, tight up to the constant for undirected uniform problems. Klein, Rao, Agrawal and Ravi (1990s) and Linial, London and Rabinovich (1995) extended the undirected theorem to general demands with an $O(\log k)$ gap. For directed graphs with general demands the gap is polynomial in $n$ (Chuzhoy and Khanna 2009), so the uniform-demand directed theorem is the setting where a logarithmic gap holds.

Setting

A directed network is a finite vertex set $V$ with $n=|V|$ nodes and a capacity $C(u,v)\ge0$ for each ordered pair, with $C(u,u)=0$; there is an edge directed from $u$ to $v$ when $C(u,v)>0$. For $U\subseteq V$ write $\bar U=V\setminus U$ and let $C(U,\bar U)=\sum_{u\in U,\,v\in\bar U}C(u,v)$ be the capacity of the edges directed from $U$ to $\bar U$.

The directed uniform multicommodity flow problem (directed UMFP) has one commodity for every ordered pair $(u,v)$ with $u\ne v$, each with demand $1$. A concurrent flow of value $\lambda$ routes $\lambda$ units of every commodity simultaneously, each edge carrying flow only in its own direction, with total flow on the edge $u\to v$ at most $C(u,v)$. The max-flow $f$ is the largest such $\lambda$.

The ratio cost of a cut is $C(U,\bar U)/(|U|\,|\bar U|)$, and the min-cut is

$$\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.$$

A distance function assigns a length $d(u,v)\ge0$ to each directed edge; $d(u,v)$ then also denotes the length of a shortest directed path from $u$ to $v$, its total weight is $W=\sum_{u,v}C(u,v)\,d(u,v)$, and the distance constraint is $\sum_{(u,v)\in V^2}d(u,v)\ge1$. The sets $\mathcal N^\Delta_{\mathrm{in}}(v,G)$ and $\mathcal N^\Delta_{\mathrm{out}}(v,G)$ are the nodes from which $v$ can be reached, respectively which can be reached from $v$, by a directed path of length at most $\Delta$. Logarithms are to base $2$.

In Lean these are DiNetwork, diCutCap, diRatio, diMinCut, diDemand, IsDiConcurrentFlow, diMaxFlow, diDist, diTotalWeight, SatisfiesDiConstraint, inBall and outBall, in the namespace LeightonRao.Directed.

Formalization targets

Goal: Theorem 12 (p. 804)

There is an absolute constant $c>0$ such that every directed UMFP on $n\ge2$ nodes satisfies

$$c\,\frac{\mathcal S}{\log n}\le f\le\mathcal S.$$

The constant is left unfixed, as in the paper's $\Omega(\cdot)$; any improvement of the constant leaves the goal intact.

Milestones

1. Weak duality (p. 804): every concurrent flow of value $\lambda$ has $\lambda|U||\bar U|\le C(U,\bar U)$ for every proper cut.
2. LP duality (§2.2, p. 796, used for directed graphs in §2.4): every feasible distance function has $W\ge f$, and an optimal one has $W=f$.
3. Lemma 13 (p. 804): for every $\Delta>0$, an ordered partition $V_1,\dots,V_r$ whose backward edges (from $V_i$ to $V_j$, $j<i$) have capacity at most $8W\log n/\Delta$, each part containing a node whose in- and out-balls of radius $\Delta$ are at least as large as the part.
4. Corollary 14 (p. 806): with $\Delta=1/4n^2$, either a node whose in- and out-balls both have at least $2n/3$ nodes, or a directed cut of ratio cost at most $8W\log n/(\Delta(n/6)(5n/6))$.
5. Lemma 15 (p. 806): a set $T$ with $|T|\ge2n/3$ and $\sum_{u\notin T}d(T,u)\ge1/4n$ or $\sum_{u\notin T}d(u,T)\ge1/4n$ gives a directed cut of ratio cost at most $12W$.
6. Lemma 16 (p. 807): a distance function satisfying the distance constraint gives a directed cut of ratio cost at most $\tfrac{1152}{5}W\log n$.

Significance

The result. Theorem 12 says that the directed sparsest cut and the directed uniform concurrent flow agree within an $O(\log n)$ factor. Since the flow is an LP, this gives an $O(\log n)$-approximation for the directed uniform sparsest cut, and through divide and conquer, polylogarithmic approximations for directed problems such as minimum feedback arc set and minimum directed cut linear arrangement (§3 of the paper). It is also the case in which a logarithmic flow–cut gap survives for digraphs: with arbitrary demands, the directed gap is polynomial.

Formalizing it. The theorem has been proved since 1988, but no part of it is formalized: Mathlib has no multicommodity flows, no directed path metrics over real lengths, and no region-growing arguments. This mission produces the directed concurrent-flow model, its LP duality, and the directed region-growing decomposition of Lemma 13, each reusable beyond this paper (directed multicut, feedback arc set, low-diameter decompositions of digraphs).

Difficulty

The obvious route copies the undirected proof: grow a ball around a node until the capacity on its boundary is small compared with the capacity inside, cut it off, and repeat. In a digraph this fails at two places. A ball of small out-radius can have large in-radius, so a piece cut off by out-distances is not small in the sense needed later; and cutting off a piece only controls the edges leaving it in one direction, so edges pointing back into earlier pieces are not paid for. Lemma 13 has to bound the capacity of all backward edges of an ordered partition while keeping each part inside both an in-ball and an out-ball around one of its own nodes. The final averaging step also changes: the undirected argument sums $d(T,u)+d(T,v)$ over symmetric pairs, which has no directed counterpart, so the distance constraint over ordered pairs has to be split between distances into one set and out of another.

Formalization scope

Vertices form a Fintype with decidable equality, and every goal-level statement assumes $n\ge2$. Commodities are ordered pairs with demand $1$; a flow is in arc form, $f_{st}(i,j)\ge0$ with conservation, and the capacity constraint is per directed edge. The max-flow is the supremum (sSup) of the achievable values $\lambda\ge0$; the min-cut is an infimum over nonempty proper subsets, since the ratio is $0/0$ otherwise. Shortest-path distances are infima over directed walks (lists of vertices along edges of positive capacity); for nonnegative lengths these equal shortest-path lengths. An unreachable pair would get Lean's junk value $0$, so every statement using $d(u,v)$ assumes strong connectivity ($C(U,\bar U)>0$ for every proper $U$), the directed analogue of the paper's standing assumption on p. 789; the balls are defined through the existence of a walk and need no such assumption. $W$ counts each directed edge once, and the distance constraint sums over ordered pairs. "We can find" is read as existence; running times are not formalized. The $\Omega$ of Theorem 12 is one absolute constant chosen before the network; the explicit constants $8$, $1152/5$ and $12$ of the milestones are the ones computed in the paper's proofs.

Two printed slips are corrected and disclosed: Lemma 13 (1) prints $1\le j<i<r$ where the proof uses $i\le r$, and the proof's last line prints $|\mathcal N^\Delta_{\mathrm{out}}(v,G)|\le|V_i|$ where the statement has $\ge$.

The statement cannot be trivialized by a degenerate cut or flow: cuts range over nonempty proper subsets, the flow's capacity constraint is directional, and the goal's constant is quantified before the network, so a constant depending on $n$ does not count.

Needed infrastructure: LP duality for the concurrent flow LP (or a direct proof of the max-flow/distance duality), shortest directed paths with real lengths, and the region-growing bookkeeping. Contributions to any milestone are welcome, as are alternative proofs of Lemma 13 by continuous region growing.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
• N. Linial, E. London and Yu. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• J. Chuzhoy and S. Khanna, Polynomial flow-cut gaps and hardness of directed cut problems, J. ACM 56(2):6, 2009. https://doi.org/10.1145/1502793.1502795

Motivation

An infinite dimensional variational problem can be described by continuous linear operators and convex functionals, yet numerical work needs finite dimensional spaces. The question is whether a solution computed in a finite dimensional approximation still approaches the solution of the original problem when the approximation is refined. Gabay and Mercier's IRIA report studies this question alongside a dual algorithm. Its Section 4 gives a convergence statement for internal approximations of the primal problem. The result is relevant to finite element methods because it identifies conditions on the discrete spaces, discrete operators, and nonsmooth part of the objective that ensure convergence of the minimizers.

The report is the June 1975 preprint of a 1976 journal paper. This mission follows the pinned report version, hal-04716124v1, whose theorem and equation numbers are used throughout. Its Section 4 first states the abstract approximation theorem and then turns to a concrete finite element construction. The abstract theorem is the target here. Gabay and Mercier, pp. 20–23.

Setting

Let $V$ and $Y$ be real Hilbert spaces, and let $A:V\to Y$ be a continuous linear operator. A continuous linear functional $b\in V'$ supplies a linear term. Let $f_2:Y\to(-\infty,+\infty]$ be a proper, convex, lower semicontinuous function. Its value may be $+\infty$, which excludes an inadmissible point. The continuous problem $({\cal P})$ is to minimize

$$J(v)=\frac12\|Av\|^2+f_2(Av)-\langle b,v\rangle,\qquad v\in V.$$

A solution has finite objective value and minimizes $J$ over all of $V$. The report's coercivity condition (2.5) supplies $\alpha>0$ such that $\|Av\|^2\ge\alpha^2\|v\|^2$ for every $v\in V$. It also assumes the interior of the effective domain of $f_2$ is nonempty. The proof of Proposition 2.1 explicitly requires a point $v_0\in V$ with $f_2(Av_0)<+\infty$; this feasibility condition is made explicit here. Gabay and Mercier, pp. 8–9.

For each approximation index $k$, let $V_k\subseteq V$ be a finite dimensional subspace and $A_k:V_k\to Y$ a continuous linear operator. The discrete problem $({\cal P}_k)$ minimizes $\frac12\|A_kw\|^2+f_2(A_kw)-\langle b,w\rangle$ over $w\in V_k$. The same $A_k$ appears in both terms involving the image of $w$. The report also describes a subspace $Y_h\subseteq Y$ containing the range of $A_h$; the abstract convergence claim uses those images only as elements of $Y$. Gabay and Mercier, pp. 20, 23.

The operator assumptions (4.1) include uniform constants $\alpha'>0$ and $M$ with $\alpha'\|w\|\le\|A_kw\|\le M\|w\|$, preservation of weak and strong limits, and $\|A_kw-Aw\|\to0$ for uniformly bounded families. The compatibility condition (4.3) requires, for each $v\in V$, points $w_k\in V_k$ with $w_k\to v$ and $f_2(A_kw_k)\to f_2(Av)$. The latter limit is extended valued when necessary. These conditions define what counts as an internal approximation for this theorem. Gabay and Mercier, p. 20.

Formalization targets

The main target is Theorem 4.1. The continuous problem has a unique solution $v^*$; the discrete problems have unique solutions for all sufficiently fine approximations; and

$$v_k^*\longrightarrow v^*\quad\text{strongly in }V.$$

The theorem's phrase “in $V_h$ strongly” is read in the common ambient space $V$, because the spaces $V_h$ vary. The claim covers every selection of discrete minimizers once they exist. The paper's conditions allow a few early discrete problems to be infeasible, so existence is asserted eventually. Gabay and Mercier, p. 21, Theorem 4.1.

The milestone list follows the report's own path from the application of Proposition 2.1 on p. 20 through the variational inequality (4.4), the bound after (4.5), weak convergence after (4.7), the estimate (4.8), and the limits (4.10)–(4.11). The equations (4.5) and (4.8) contain printing slips; their milestone excerpts preserve the printed text, while their formal statements use the mathematically consistent readings explained with each item. Gabay and Mercier, pp. 21–22.

Significance

The theorem gives a precise guarantee for a family of finite dimensional problems: a computed minimizer is meaningful as an approximation to the unique solution of the infinite dimensional problem when the discretization satisfies the stated conditions. The operator $A_k$ may differ from the restriction of $A$ to $V_k$, and the nonsmooth term $f_2$ may assign $+\infty$ outside its domain. The conclusion therefore covers settings in which simply restricting the continuous objective to a subspace would describe the wrong numerical problem. Gabay and Mercier, pp. 20–23.

The result is proved in the report; the remaining task is a machine checked proof of the abstract approximation theorem and its cited intermediate claims. A formal development would also leave reusable statements about extended valued convex minimization, weak convergence of Hilbert space sequences, and uniformly consistent discrete operators. This proposal supplies statements for those claims; it does not claim that they already have machine checked proofs.

Difficulty

Strong convergence cannot be read off from a bound on the discrete solution norms. Uniform boundedness yields only access to weak limits in the Hilbert space; the solution's images and the nonsmooth objective must still behave correctly under the varying operators. Weak convergence of $v_k^*$ alone also does not imply convergence in norm. A proof must keep the weak limit, the lower semicontinuity of $f_2$, and the discrepancy between $A_k$ and $A$ aligned under the same approximation assumptions. The fact that $f_2$ may be infinite makes unguarded subtraction of its values invalid. Gabay and Mercier, pp. 21–22.

Formalization scope

Lean uses real complete inner product spaces for $V$ and $Y$, continuous linear maps for $A$ and $A_k$, and StrongDual ℝ V for $b$. The index $k\to\infty$ represents a sequence of mesh parameters $h_k\to0$; the report's convergence claims are sequential. Each $V_k$ is finite dimensional. The codomain spaces $Y_h$ are suppressed through their inclusions in $Y$. Weak convergence uses all Hilbert inner products as tests, while “strongly” means convergence in the norm topology.

The function $f_2$ takes values in EReal, with properness excluding $-\infty$. Its limit in (4.3) uses the extended real topology. The quadratic term is real valued. A solution must have a finite objective value, and the continuous problem must have a feasible point. The section's interior-domain assumption (2.4) is retained even though the abstract proof does not use it. Condition (4.1)(iv) quantifies over every uniformly bounded family. These choices rule out the vacuous interpretation in which all continuous or discrete objective values are $+\infty$.

The report's $f_1(y)=\frac12\|y\|^2$ automatically satisfies the earlier gradient monotonicity requirement (2.3). The published InertialFB.IFB.ConvexAnalysis definition provides properness, convexity, and weak convergence with matching conventions. The new local definition supplies the two objectives, solution predicates, and approximation hypotheses. Contributions proving the goal and its milestones are welcome; separate treatments of the concrete triangulation and quadrature construction of Proposition 4.1 are outside this mission. Gabay and Mercier, pp. 20–26.

Selected references

• D. Gabay and B. Mercier, A dual algorithm for the solution of non linear variational problems via finite element approximation, IRIA Rapport de Recherche no. 126, June 1975, hal-04716124v1. This report is the version whose numbering the mission uses.
• D. Gabay and B. Mercier, A dual algorithm for the solution of nonlinear variational problems via finite element approximation, Computers & Mathematics with Applications 2 (1976) 17–40, doi:10.1016/0898-1221(76)90003-1. The journal version; its numbering is not used here.

Why multicommodity max-flow and min-cut

For a single commodity, the Ford–Fulkerson theorem says that the maximum flow between two nodes equals the minimum capacity of a cut separating them. Many routing and partitioning problems involve many source–sink pairs at once, and for those the equality fails: the largest fraction of every demand that can be routed simultaneously can be strictly smaller than the sparsest cut. Leighton and Rao (J. ACM 1999, building on their FOCS 1988 paper) proved that the gap is at most logarithmic for broad classes of demand patterns, and turned the proof into the first $O(\log n)$-approximation algorithms for sparsest cut, balanced separators, minimum feedback arc set, crossing number and VLSI layout problems.

This mission formalizes Section 2.3 of the paper: the extension of the uniform max-flow min-cut theorem to product multicommodity flow problems (PMFPs), where the demand between two nodes is the product of their node weights.

Timeline.

• 1956: Ford and Fulkerson, single-commodity max-flow = min-cut.
• 1963: Hu, equality for two commodities.
• 1988: Leighton and Rao (FOCS), $\Theta(\log n)$ gap for uniform demands; the product-demand extension, pointed out to them by Shmoys, Tardos and Sinclair, appears in the journal version (1999), Theorem 7.
• 1993–1995: Klein–Agrawal–Ravi–Rao, Garg–Vazirani–Yannakakis, Linial–London–Rabinovich and Aumann–Rabani extend the $O(\log k)$ gap to arbitrary demands with $k$ commodities.

Setting

A network is a finite vertex set $V$ with a symmetric capacity $C(u,v)\ge0$ on each pair, zero on the diagonal; $\{u,v\}$ is an edge when $C(u,v)>0$. For $U\subseteq V$, the cut capacity is $C(U,\bar U)=\sum_{u\in U,\,v\notin U}C(u,v)$. The network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$.

A PMFP is given by a node weighting $\pi:V\to\mathbb R_{\ge0}$. Write $\mathcal P$ for the set of nodes with $\pi(u)\ne0$, $p=|\mathcal P|$, and $\pi(U)=\sum_{u\in U}\pi(u)$. As in the paper, the weights are normalized so that $\pi(V)=p$. Every pair $\{u,v\}$ is a commodity with demand $\pi(u)\pi(v)$; there are $k=\binom p2$ commodities with nonzero demand. The uniform problem is $\pi\equiv1$.

The max-flow $f$ is the largest $\lambda$ such that $\lambda\pi(u)\pi(v)$ units of every commodity can be routed simultaneously, with the total flow on each edge (both directions) at most its capacity. The min-cut is

$$\mathcal S=\min_{U:\ \pi(U)>0,\ \pi(\bar U)>0}\frac{C(U,\bar U)}{\pi(U)\,\pi(\bar U)},$$

the quotient being the weighted ratio cost of the cut $\langle U,\bar U\rangle$.

The dual objects are distance functions: lengths $d(e)\ge0$ on the edges, with total weight $W=\sum_eC(e)d(e)$; $d(u,v)$ is the shortest-path distance and $d(T,u)=\min_{t\in T}d(t,u)$. The weighted distance constraint is $\sum_{\{u,v\}\in\mathcal P^2}\pi(u)\pi(v)d(u,v)\ge1$.

Formalization targets

Goal: Theorem 7 (pp. 801–802)

There is an absolute constant $c>0$ such that every normalized PMFP with $p\ge2$ on a connected network satisfies

$$\frac{c\,\mathcal S}{\log_2\max(k,2)}\le f\le\mathcal S .$$

The goal leaves the constant unfixed, which is the paper's $\Omega(\cdot)$.

Milestones, in the order the proof uses them

1. Weak duality (§1.2, pp. 789–790): $f\,\pi(U)\pi(\bar U)\le C(U,\bar U)$ for every cut with positive weight on both sides.
2. LP duality for the PMFP (p. 802 with p. 796): distance functions satisfying the weighted constraint have $W\ge f$, and one attains $W=f$.
3. Lemma 8 (p. 802): a partition whose components meeting $\mathcal P$ have radius at most $\Delta$ and whose cross capacity is at most $4W\log p/\Delta$.
4. Corollary 9 (p. 802): either a set $T$ of radius $1/2p^2$ with $\pi(T)\ge2p/3$, or a cut of weighted ratio cost $O(W\log p)$.
5. Lemma 10 (p. 802): a heavy set $T$ far on average from the remaining weight yields a cut of weighted ratio cost $O(W)$.
6. Lemma 11 (p. 803): a distance function satisfying the weighted constraint yields a cut of weighted ratio cost $O(W\log p)$.

Stronger companions

• $\mathcal S\le36\log_2\max(k,2)\cdot f$, the constant of the paper's proof.
• Theorem 7 without the normalization $\pi(V)=p$, which the paper assumes "without loss of generality".

Significance

Theorem 7 bounds the multicommodity flow–cut gap by $O(\log k)$ for every product demand pattern, so an optimal dual distance function certifies a cut within $O(\log k)$ of the sparsest weighted cut. The paper itself applies it to reversible Markov chains (§3.27, p. 827). There the node weights are the stationary probabilities, and Theorem 7 shows that the inverse conductance and the resistance of a chain agree up to a $\Theta(\log p)$ factor, where $p$ is the number of states with positive stationary probability.

Theorem 7 was proved in 1988–1999 and is subsumed, up to the constant, by the general $O(\log k)$ bound for arbitrary demands (Linial–London–Rabinovich 1995; Aumann–Rabani 1998). It has no machine-checked proof, and neither has any of its milestones. A complete development would also be the first formal treatment on Prove2Me of concurrent multicommodity flow, its LP dual, and region-growing (low-diameter) decompositions, which recur across approximation algorithms and metric embeddings.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the work. Rounding an optimal dual distance function to a cut fails directly: thresholding distances from a single node gives no control on the ratio when the weight is spread out. The paper's argument needs a decomposition of the graph into components of small radius that cuts little capacity, with a loss of only $\log p$, not $\log n$: the regions must be grown from weighted nodes only, while the many zero-weight nodes still sit inside the graph and its capacities. It must then separately handle the case where one component carries two thirds of the weight. Formally, the LP duality step alone requires a strong-duality statement for a linear program with one constraint per path, exponentially many, which Mathlib does not provide in this form.

Formalization scope

All objects live in the namespace LeightonRao.Product in a single definitions file.

• Network and graph. A network is a symmetric nonnegative capacity function on a finite type with zero diagonal. The graph has an edge where the capacity is positive.
• Commodities. One commodity per ordered pair $u\ne v$, with demand $\tfrac12\pi(u)\pi(v)$ each way (the paper's footnote 7). The total demand of a pair is then $\pi(u)\pi(v)$, and the demand separated by $U$ is $\pi(U)\pi(\bar U)$.
• Max-flow. Flows are arc flows per commodity. The max-flow is the supremum of the feasible values $\lambda\ge0$.
• Min-cut. The min-cut ranges only over cuts with $\pi(U)>0$ and $\pi(\bar U)>0$. On the other cuts the paper's quotient is undefined; reading it with Lean's division by zero would make $\mathcal S=0$ and the goal trivial.
• Distances, radius, cross capacity. Graph distances are infima of walk lengths. The radius of a component is measured by walks inside the component. Cross capacity is the capacity between different parts of a Finpartition.
• Logarithms. $\log$ is $\log_2$ (the paper's footnote 3). For $p=2$ there is one commodity and $\log k=0$, so the goal uses $\log_2\max(k,2)$.
• Constants. The $O(\cdot)$ constants of the milestones are the ones computed in the paper's proofs: $36$ in Corollary 9 and Lemma 11, $6$ in Lemma 10.
• Hypotheses added to the page, each disclosed in its statement:
  • $\Delta>0$ in Lemma 8, where the page says $\Delta\ge0$ but divides by $\Delta$;
  • $p\ge2$ in Lemma 8, which is false for $p=1$;
  • the weighted ratio cost in Lemma 10, as its proof and its use in Lemma 11 require.
• Not formalized. The polynomial-time content of "we can find" is not formalized; each such claim is an existence statement.

Contributions are welcome at every level:

• proofs of the milestones;
• a general strong-duality lemma for concurrent flow, reusable for the uniform, directed and short-path missions of this series;
• a reusable region-growing decomposition lemma.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• T. Leighton and S. Rao, An approximate max-flow min-cut theorem for uniform multicommodity flow problems with applications to approximation algorithms, FOCS 1988, 422–431. https://doi.org/10.1109/SFCS.1988.21958
• N. Garg, V. V. Vazirani and M. Yannakakis, Approximate max-flow min-(multi)cut theorems and their applications, SIAM J. Comput. 25(2):235–251, 1996. https://doi.org/10.1137/S0097539793243016
• N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• Y. Aumann and Y. Rabani, An O(log k) approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27(1):291–301, 1998. https://doi.org/10.1137/S0097539794285983
• F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620

Motivation

Convex programs with inequality constraints arise when a decision must meet capacity, resource, or performance limits. Their Lagrange multipliers assign a price to each constraint. Finding an optimal multiplier gives a dual certificate and can guide a primal optimization method. Classical quadratic multiplier methods update these prices through a particular penalty. Eckstein's 1993 paper places a broader family of multiplier updates inside the theory of Bregman proximal point algorithms, allowing a nonquadratic function to shape each step (Eckstein 1993, §4.2).

The result here concerns the inequality constrained case, where multiplier vectors must be componentwise nonnegative. Eckstein identifies a monotone conjugate that incorporates this restriction into the primal penalty and proves that the resulting multiplier sequence converges to an optimal multiplier when one exists. The paper also studies primal limit points and the behavior when no optimal multiplier exists (Eckstein 1993, Theorem 7 and proof, pp. 216–219).

Setting

Let $C\subseteq\mathbb R^n$ be closed, nonempty, and convex. Let $f,g_1,\ldots,g_m$ be proper lower semicontinuous convex functions, finite on $C$. The primal problem is to minimize $f(x)$ over $x\in C$ subject to $g_i(x)\le 0$ for every $i$. Write $g(x)=(g_1(x),\ldots,g_m(x))$. A point solves the problem only when it lies in $C$, satisfies every inequality, and has no larger objective value than any other feasible point.

For a nonnegative multiplier $p$, the dual functional is $d(p)=\inf_{x\in C}\{f(x)+\langle p,g(x)\rangle\}$; it equals $-\infty$ outside the nonnegative orthant. A multiplier $p^*$ is optimal when it maximizes $d$. The standing assumption that $d$ is not identically $-\infty$ makes this dual functional a meaningful proper concave object (Eckstein 1993, p. 215).

A Bregman function $h$ has an open zone $S$. It is continuously differentiable there, strictly convex and continuous on $\overline S$, and satisfies the boundedness and sequential conditions of Definition 1. Its Bregman distance is $D_h(u,v)=h(u)-h(v)-\langle\nabla h(v),u-v\rangle$, with $u\in\overline S$ and $v\in S$. The zone contains the strict positive orthant, and the image of its gradient contains that orthant. Its monotone conjugate is $h^{*+}(z)=\sup_{p\ge0}\{\langle p,z\rangle-h(p)\}$. Lemma 3 establishes that this function is finite and differentiable everywhere under these assumptions (Eckstein 1993, pp. 205, 215–216).

Given positive step sizes $c_k$ bounded away from zero, recursion (11) chooses $x^{k+1}$ as a minimizer over $C$ of $f(x)+c_k^{-1}h^{*+}(\nabla h(p^k)+c_kg(x))$, then sets $p^{k+1}=\nabla h^{*+}(\nabla h(p^k)+c_kg(x^{k+1}))$. The theorem assumes an infinite sequence conforming to these recursions; it does not assert that each minimizer exists for arbitrary data.

Formalization targets

Multiplier convergence

The goal is Eckstein's Theorem 7. If the dual problem has an optimal multiplier, then the multiplier sequence converges to one:

$$\exists p^*\in\operatorname*{argmax}d\quad\text{such that}\quad p^k\longrightarrow p^*.$$

When every $g_i$ is continuous on $C$ and $S$ contains the closed nonnegative orthant, each subsequential limit of the primal iterates solves the constrained problem. Under the same zone condition, the multiplier sequence is unbounded if the dual has no optimal multiplier. The printed theorem says “if (10) has no solution” in this last clause; its proof on p. 218 establishes the no-optimal-multiplier condition, which is the version formalized here.

Supporting targets

The milestones include the representations of $h^{*+}$ in Lemma 2, the appendix results governing recession directions and the monotone conjugate, Lemma 3's global finiteness and differentiability, the subdifferential chain rule, and the Bregman proximal point result of Theorem 1. They also capture the paper's claims that recursion (11) is a Bregman proximal point run for $\partial(-d)$ and that primal limit points meet the feasibility, complementarity, and Lagrangian conditions.

Significance

The theorem supplies a convergence guarantee for nonquadratic methods of multipliers with inequality constraints. It separates the dual conclusion, which uses the strict positive orthant condition, from the primal limit and unboundedness conclusions, which additionally require the closed orthant to lie in the zone. This distinction lets a Bregman function whose zone excludes boundary points still yield dual convergence when optimal multipliers exist (Eckstein 1993, Theorem 7, pp. 216–218).

Eckstein proved this theorem on paper. The mission asks for machine checked proofs of its precise statements and the supporting results; the draft statements compile but their proofs remain open. A completed development would also provide reusable finite dimensional infrastructure for extended-real convex functions, monotone conjugates, Bregman distances, and convex-analytic multiplier conditions.

Difficulty

A direct appeal to ordinary proximal point convergence does not identify the update in (11) as a proximal step: the primal minimization uses $h^{*+}$, whereas the operator of interest is the subdifferential of the negative dual functional. The nonnegative orthant also introduces boundary behavior absent from the equality constrained case. The link requires precise conjugacy and subdifferential statements, including a globally finite monotone conjugate, before Theorem 1 can apply (Eckstein 1993, pp. 215–218). For primal limit points, the issue is to pass from optimality of each primal subproblem to feasibility, complementarity, and minimization of the limiting Lagrangian.

Formalization scope

Lean uses finite dimensional real inner product spaces for the general proximal point theorem and EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m) for the primal and multiplier spaces. Functions that the paper regards as extended-valued are represented by EReal; their properness excludes $-\infty$. The infimum defining $d$ and the supremum defining $h^{*+}$ remain extended-real operations, so an infinite value cannot silently become zero. Real values are extracted from $h^{*+}$ in recursion (11) only because Lemma 3 asserts finiteness everywhere.

The real function $h$ is total in Lean but constrained only on $\overline S$; its gradient is evaluated only at points in $S$. Every multiplier iterate is explicitly in $S$. The initial primal value $x^0$ is unused by recursion (11). The Bregman proximal point recursion is represented by its equivalent inclusion (4), and a “limit point” is a subsequential limit. The sequential condition (vi) of Definition 1 is stated for $x^k\in\overline S$, the natural first-argument domain of $D_h$. The Appendix's essential strict convexity means strict convexity on convex subsets of the subdifferential domain. Its recession direction uses the stated limit inferior condition.

Lemma A4's printed unconditional claim that its composite $G$ is proper lacks a finite-value witness. The formal statement keeps convexity of $G$ unconditional and states properness at a point $x_0$ where all inner functions and the outer function are finite; differentiability of the outer function there is expressed with local finiteness of its extended-real value. At a zero coefficient, its corresponding subgradient term contributes zero without requiring a subgradient to exist. These conditions expose rather than hide the domain issue. The formulation rules out an arbitrary multiplier sequence, an all-space supremum, or a minimization over infeasible points. Contributions proving the milestones, improving shared convex analysis libraries, and checking the boundary conventions are welcome.

Selected references

• Jonathan Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI:10.1287/moor.18.1.202.

Motivation

The Nelder–Mead simplex method (Nelder and Mead, 1965) is one of the most widely used methods for minimizing a function without derivatives. It is the default unconstrained derivative-free minimizer in several numerical libraries (fminsearch in MATLAB, method="Nelder-Mead" in SciPy) and is used routinely in chemistry, engineering and statistics, where the objective is a simulation or a measurement whose gradient is unavailable.

Its theory lags far behind its use. Until 1998 there was no convergence result for the method as stated, in any dimension. Lagarias, Reeds, Wright and Wright (SIAM J. Optim. 9 (1998) 112–147) gave the first: in dimension one, on strictly convex functions with bounded level sets, the method converges to the minimizer whenever the product of its reflection and expansion coefficients is at least one. McKinnon (SIAM J. Optim. 9 (1998) 148–158) showed in the same issue that in dimension two the method can converge to a non-stationary point even for strictly convex smooth functions, so results of this kind cannot be expected in general.

Timeline:

• 1965: Nelder and Mead introduce the method (Comput. J. 7, 308–313).
• 1998: Lagarias, Reeds, Wright and Wright prove convergence in dimension 1 for strictly convex functions when $\rho\chi \ge 1$, $M$-step linear convergence when $\rho = 1$, and that the simplex diameter tends to zero in dimension 2 with the standard coefficients.
• 1998: McKinnon's family of strictly convex functions in dimension 2 on which the method converges to a non-minimizer.
• 2012: Lagarias, Poonen and Wright prove convergence of a restricted variant (no expansion steps) for a class of strictly convex functions in dimension 2 (SIAM J. Optim. 22 (2012) 501–532).

This mission formalizes the one-dimensional convergence theorem.

Setting

Let $f : \mathbb R \to \mathbb R$. In dimension one a Nelder–Mead simplex $\Delta_k$ is a pair of distinct points $x_1^{(k)}, x_2^{(k)}$, ordered so that $f(x_1^{(k)}) \le f(x_2^{(k)})$: $x_1$ is the best and $x_2$ the worst vertex. Four coefficients are fixed in advance, reflection $\rho$, expansion $\chi$, contraction $\gamma$ and shrink $\sigma$, satisfying the conditions (2.1) of the paper:

$$\rho > 0,\quad \chi > 1,\quad \chi > \rho,\quad 0 < \gamma < 1,\quad 0 < \sigma < 1.$$

From $\Delta = (x_1, x_2)$ the method forms the trial points

$$x_r = x_1 + \rho(x_1 - x_2),\quad x_e = x_1 + \rho\chi(x_1 - x_2),\quad x_c = x_1 + \rho\gamma(x_1 - x_2),\quad x_{cc} = x_1 - \gamma(x_1 - x_2).$$

With $f_1 = f(x_1)$, $f_2 = f(x_2)$, $f_r = f(x_r)$ and so on, one iteration does the following:

1. if $f_r < f_1$, it expands, accepting $x_e$ if $f_e < f_r$ and $x_r$ otherwise;
2. if $f_1 \le f_r < f_2$, it tries an outside contraction, accepting $x_c$ if $f_c \le f_r$;
3. if $f_r \ge f_2$, it tries an inside contraction, accepting $x_{cc}$ if $f_{cc} < f_2$;
4. if a contraction is rejected, it shrinks, replacing $x_2$ by $x_1 + \sigma(x_2 - x_1)$.

The worst vertex is discarded, and the accepted point $v$ becomes the new best vertex if $f(v) < f_1$ and the new worst vertex otherwise (the paper's tie-breaking rule). The diameter of the simplex is $\operatorname{diam}(\Delta_k) = |x_1^{(k)} - x_2^{(k)}|$. The function $f$ is strictly convex, and it has bounded level sets: $\{x : f(x) \le \mu\}$ is bounded for every $\mu$. It then has a unique minimizer $x_{\min}$.

Formalization targets

Goal: Theorem 4.1

If, in addition to (2.1), $\rho\chi \ge 1$, then for every nondegenerate initial simplex

$$\lim_{k\to\infty} x_1^{(k)} = x_{\min} \quad\text{and}\quad \lim_{k\to\infty} x_2^{(k)} = x_{\min}.$$

The goal names no rate and no constant; it is the qualitative statement the paper proves.

Milestones

• Lemma 4.1: three properties of strictly convex functions on $\mathbb R$ (an up–down–up pattern brackets $x_{\min}$; $f$ increases along rays leaving $x_{\min}$; $f$ is continuous).
• Lemma 3.5, case $n = 1$: no shrink step ever occurs.
• Lemma 4.2: with $\rho\chi \ge 1$ there is a first iteration $K$ with $f_2^{(K)} \ge f_1^{(K)} \le f_e^{(K)}$, and then $x_{\min}$ lies strictly between $x_2^{(K)}$ and $x_e^{(K)}$.
• Lemma 4.3: with $N_{NM} = \max(1/(\rho\gamma), \rho/\gamma, \rho\chi, \chi - 1)$, the proximity property $x_{\min} \in \operatorname{int}(x_2^{(k)}, x_1^{(k)} + N_{NM}(x_1^{(k)} - x_2^{(k)})]$ persists from one iteration to the next.
• Lemma 4.4: the limits $f_1^*$, $f_2^*$ of the vertex values coincide.
• Lemma 4.5: $\operatorname{diam}(\Delta_k) \to 0$.
• (4.9): the proximity property gives $|x_{\min} - x_1^{(k)}| \le N_{NM} \operatorname{diam}(\Delta_k)$.

A further item states the paper's remark that when $\rho\chi < 1$ the vertices stay within $\operatorname{diam}(\Delta_0)/(1 - \rho\chi)$ of $x_1^{(0)}$, so convergence to $x_{\min}$ fails when the minimizer is farther away.

Significance

Theorem 4.1, together with the remark on $\rho\chi < 1$, identifies $\rho\chi \ge 1$ as the right condition for global convergence of the one-dimensional method, and it holds for all contraction coefficients and for infinitely many expansion steps. It is the base case of the low-dimensional theory: the linear-rate result for $\rho = 1$ (Theorem 4.2) builds on the same bracketing and proximity lemmas, and McKinnon's example shows that nothing comparable holds in dimension two.

The result is proved in the paper; no machine-checked proof of any convergence property of the Nelder–Mead method is known to exist. A formalization gives a precise, executable definition of the algorithm with its tie-breaking rules, which the literature states in several inequivalent variants, and it checks a proof with a known gap: the bound on $K$ printed in Lemma 4.2 is false (see below), so the published argument cannot be followed line by line.

Difficulty

The obvious argument, that the best value decreases and so the best vertex converges, fails twice. The best vertex may stall while contractions continue, and the diameter can grow, by the factor $\rho\chi$ at every expansion step, so there is no monotone potential. The proof must show that the minimizer is eventually trapped in an interval proportional to the current diameter (Lemmas 4.2, 4.3), and separately that the diameter tends to zero whatever the sequence of moves (Lemmas 4.4, 4.5); the latter needs a case analysis of infinite runs of contractions and of the two limit points of a strictly convex level set.

Formalization scope

The Lean development lives in the namespace NelderMeadLD.Conv1D. The simplex is an ordered pair p : ℝ × ℝ with p.1 $= x_1$ (best) and p.2 $= x_2$ (worst); one iteration step is a function of the pair, and the run is its $k$-fold iterate from the initial pair. Committed conventions:

• the expansion step accepts the better of $x_r$ and $x_e$; the outside contraction is accepted on $f_c \le f_r$, the inside contraction on $f_{cc} < f_2$;
• a new point with value equal to $f_1$ becomes the worst vertex (the page's printed formula for the insertion index always gives the last index; the words and the example on p. 118 describe the rule used);
• the initial pair is nondegenerate, $x_1^{(0)} \ne x_2^{(0)}$, and ordered, $f(x_1^{(0)}) \le f(x_2^{(0)})$;
• strict convexity is StrictConvexOn ℝ Set.univ f, bounded level sets are Bornology.IsBounded {x | f x ≤ μ} for every μ, and the minimizer is a binder with ∀ y, f xmin ≤ f y;
• every statement of §4 carries all five conditions (2.1), the standing assumption of the one-dimensional analysis, even where the lemma names fewer; $\rho\chi \ge 1$ is added only where the paper states it;
• limits are stated with Tendsto; Lemma 4.4 asserts the existence of a common limit of both value sequences.

The printed bound $K \le |x_{\min} - x_1^{(0)}| / \operatorname{diam}(\Delta_0)$ of Lemma 4.2 is false ($f(x) = (x-5)^2$, $\Delta_0 = (3, 0)$, $\rho = 1$, $\chi = 1.1$) and is not stated; the existence and minimality of $K$ and the bracketing are. A formalization that drops nondegeneracy or the ordering of the initial pair, or quantifies $x_{\min}$ over an arbitrary point, is not this theorem: with $x_1^{(0)} = x_2^{(0)}$ every iteration is a shrink to the same point and the goal is false.

Needed infrastructure: elementary facts on strictly convex functions of one real variable (three-point bracketing, monotonicity beyond the minimizer, continuity), and bookkeeping for iterates of a piecewise-defined map. Lemma 4.1 is reusable beyond this mission. Contributions are welcome on every milestone, independently: Lemmas 4.4 and 4.5 do not use $\rho\chi \ge 1$.

Selected references

• J. C. Lagarias, J. A. Reeds, M. H. Wright, P. E. Wright, Convergence properties of the Nelder–Mead simplex method in low dimensions, SIAM J. Optim. 9(1) (1998), 112–147. https://doi.org/10.1137/S1052623496303470
• J. A. Nelder, R. Mead, A simplex method for function minimization, Comput. J. 7(4) (1965), 308–313. https://doi.org/10.1093/comjnl/7.4.308
• K. I. M. McKinnon, Convergence of the Nelder–Mead simplex method to a nonstationary point, SIAM J. Optim. 9(1) (1998), 148–158. https://doi.org/10.1137/S1052623496303482
• J. C. Lagarias, B. Poonen, M. H. Wright, Convergence of the restricted Nelder–Mead algorithm in two dimensions, SIAM J. Optim. 22(2) (2012), 501–532. https://doi.org/10.1137/110830150

Motivation

The method of multipliers (augmented Lagrangian method) of Hestenes and Powell is one of the standard algorithms for constrained convex optimization. Each iteration minimizes the Lagrangian plus a quadratic penalty on the constraint residual, then updates the multiplier estimate. Rockafellar showed in 1976 that this method is the proximal point algorithm applied to the dual problem (Rockafellar, Math. Oper. Res. 1976), which explains its global convergence for convex programs without differentiability or constraint qualifications on the primal side.

The quadratic penalty is not the only one used in practice. Exponential and other nonquadratic penalties produce twice-differentiable augmented Lagrangians and were studied by Kort and Bertsekas and by Tseng and Bertsekas. Eckstein (Math. Oper. Res. 18(1), 1993, 202–226) gave a uniform convergence theory for such methods. He replaces the squared Euclidean distance in the proximal point algorithm by the D-function of a Bregman function $h$, proves convergence of the resulting algorithm for every maximal monotone operator (Theorem 1), and then derives nonquadratic multiplier methods by applying it to the dual of a convex program. This mission covers the linear-equality-constrained case, §4.1 and Theorem 6 of that paper.

Setting

Let $f : \mathbb R^n \to (-\infty, +\infty]$ be convex and lower semicontinuous, let $A$ be an $m \times n$ matrix, $b \in \mathbb R^m$, and $X \subseteq \mathbb R^n$ closed and convex, with $\inf\{f(x) \mid x \in X\} < \infty$. The problem is

$$\text{minimize } f(x) \quad\text{such that}\quad Ax = b,\ x \in X. \tag{7}$$

Write $\delta_X$ for the indicator function of $X$ ($0$ on $X$, $+\infty$ off $X$) and $f_X = f + \delta_X$. The dual functional is

$$d(p) = \inf_{x \in X}\bigl\{ f(x) + \langle p, Ax - b\rangle \bigr\}, \qquad p \in \mathbb R^m,$$

assumed not identically $-\infty$. An optimal multiplier (Lagrange multiplier) is a maximizer of $d$ over $\mathbb R^m$.

For an open set $S$, a Bregman function with zone $S$ is a function $h : \bar S \to \mathbb R$ that is continuously differentiable on $S$, strictly convex and continuous on $\bar S$, and satisfies the level-set and limit conditions (iv)–(vi) of Definition 1 on its D-function $D_h(x, y) = h(x) - h(y) - \langle \nabla h(y), x - y \rangle$. Here the zone is all of $\mathbb R^m$, and $\nabla h$ is assumed onto $\mathbb R^m$. Let $h^*(z) = \sup_p\{\langle p, z\rangle - h(p)\}$ be the convex conjugate of $h$, and let $c_k > 0$ with $\inf_k c_k > 0$. The nonquadratic method of multipliers generates $\{(x^k, p^k)\}$ by

$$x^{k+1} \in \operatorname*{arg\,min}_{x \in X}\Bigl\{ f(x) + \tfrac{1}{c_k}\, h^*\bigl(\nabla h(p^k) + c_k(Ax - b)\bigr)\Bigr\}, \qquad p^{k+1} = \nabla h^*\bigl(\nabla h(p^k) + c_k(Ax^{k+1} - b)\bigr). \tag{9}$$

For $h(p) = \frac12\|p\|^2$ this is the classical method of multipliers. A run of the general Bregman proximal point algorithm for an operator $T$ is a sequence with $\frac{1}{c_k}(\nabla h(x^k) - \nabla h(x^{k+1})) \in T(x^{k+1})$ for all $k$.

Formalization targets

Goal: Theorem 6 (pp. 212–213)

Under the assumptions above:

$$\exists\, p^\star \text{ optimal} \;\Longrightarrow\; p^k \to \text{some optimal multiplier, and every limit point of } \{x^k\} \text{ solves (7)};$$ $$\nexists\, p^\star \text{ optimal} \;\Longrightarrow\; \{p^k\} \text{ is unbounded}.$$

The statement fixes no penalty: it holds for every Bregman function with zone $\mathbb R^m$ and surjective gradient. It makes no claim that $\{x^k\}$ converges, which is false in general.

Milestones

1. Theorem 1 (pp. 206–207): for a maximal monotone $T$ and a Bregman function $h$ with zone $S$, $\bar S \supseteq \operatorname{dom} T$, a run of the Bregman proximal point algorithm converges to a zero of $T$ when one exists, under either (C1) $S \supseteq \overline{\operatorname{dom} T}$ or (C2) $T = \partial f$ for a closed proper convex $f$. If $T$ has no zero and (C1) holds, the run is unbounded.
2. Proof of Theorem 6, p. 213: the multipliers produced by (9) form a Bregman proximal point run on $\partial(-d)$,

$$p^{k+1} = \bigl(\nabla h + c_k \partial(-d)\bigr)^{-1}\bigl(\nabla h(p^k)\bigr).$$

3. Proof of Theorem 6, p. 214: if $p^k \to p^\star$ with $p^\star$ optimal, then $Ax^k \to b$, and every limit point $x^\infty$ of $\{x^k\}$ satisfies $Ax^\infty = b$, $-A^{\mathsf T}p^\star \in \partial f_X(x^\infty)$, and solves (7).

An additional item states the existence clause of Theorem 6: if the row space of $A$ meets $\operatorname{ri}(\operatorname{im} \partial(f + \delta_X))$, or $f$ and $X$ are polyhedral and the row space meets $\operatorname{im} \partial(f + \delta_X)$, then (9) has an infinite run from every starting point $(x^0, p^0)$.

Significance

Theorem 6 gives global convergence of a whole family of augmented Lagrangian methods at once, with the penalty chosen through $h$. For instance, Example 5 of the paper obtains the method with penalty $\frac{1}{r c_k}\sum_i |\mu_i + c_k(A_i x - b_i)|^r$ for any $r > 1$. Its multiplier sequence behaves exactly as the dual proximal point iterates do, and it detects dual unsolvability through divergence of $\{p^k\}$. Primal limit points are optimal without any assumption beyond existence of a Lagrange multiplier.

The result has a published proof (Eckstein 1993) but, to our knowledge, no machine-checked proof. Formalizing it requires a formal treatment of Bregman functions and of the Bregman proximal point algorithm (Theorem 1). It also requires the subdifferential calculus of the dual functional: conjugates, the chain rule $\partial(g \circ A^{\mathsf T})$, and the inverse relation between $\nabla h$ and $\nabla h^*$. The milestones isolate the reduction of (9) to Theorem 1 and the primal recovery argument, each of which can be proved independently of the others.

Difficulty

The reduction step is where a direct argument fails. Showing that $p^{k+1}$ is a proximal point of $\partial(-d)$ needs the inclusion $-(Ax^{k+1} - b) \in \partial(-d)(p^{k+1})$, where $-d(p) = (f_X)^*(-A^{\mathsf T}p) + \langle b, p\rangle$ is a composition of a conjugate with a linear map. The subdifferential chain rule holds with equality only under a qualification condition. The argument must therefore use only the inclusion that holds unconditionally, together with the optimality condition for the $x$-subproblem, which needs differentiability of $h^*$ everywhere (supplied by $\operatorname{im} \nabla h = \mathbb R^m$ and strict convexity of $h$). On the primal side, $\{x^k\}$ need not be bounded or convergent, so primal optimality can only be asserted for limit points, through closedness of the graph of $\partial f_X$. Theorem 1 itself rests on the Bregman conditions (iv)–(vi), which replace the Fejér monotonicity of the Euclidean proximal point argument.

Formalization scope

• $\mathbb R^k$ is EuclideanSpace ℝ (Fin k). $A$ is a continuous linear map $\mathbb R^n \to \mathbb R^m$ (equivalent to an $m \times n$ matrix), and $A^{\mathsf T}$ is its adjoint. Theorem 1 is stated on any finite-dimensional real inner product space.
• Functions into $(-\infty, +\infty]$ are EReal-valued with "never $-\infty$" as a hypothesis. $\partial f$ uses the published IsSubgradient; convexity is convexity of the epigraph (IsConvexFn). Maximal monotonicity, dom and zer are the published ThreeOpSplitting.Convergence definitions. The conjugate $h^*$ is the published fenchelConjugate, an EReal supremum.
• (9) uses the real value of $h^*$. This is faithful because $\operatorname{im}\nabla h = \mathbb R^m$ makes $h^*$ finite everywhere. Finiteness of $h^*$ is a consequence, never a hypothesis. The arg min in (9) is a minimality predicate, not a choice function, since the minimizer need not be unique.
• Recursion (3) is encoded through its equivalent form (4). Condition (vi) of Definition 1 is stated on the natural domain $\bar S \times S$ of $D_h$.
• "Limit point" means subsequential limit, and "unbounded" means the range of the sequence is not bounded. In the existence clause, ri is Mathlib's intrinsicInterior, and polyhedral sets and functions are finite intersections of closed half-spaces (for functions, of the epigraph).
• The paper's typo "monontone" in Theorem 1 is read as "monotone".
• The convergence claims must not be weakened to their trivial instances. A formalization that assumes $\{x^k\}$ converges, or adds finiteness of $h^*$ or boundedness of $\{p^k\}$ as a hypothesis, or encodes (9) with a choice function, does not state Theorem 6.
• Reusable beyond this mission: the Bregman function structure and Theorem 1 (shared with the other missions of this series), and the dual-functional and conjugate facts for linearly constrained programs. Contributions toward the conjugate calculus ($\nabla h^* = (\nabla h)^{-1}$, the chain rule inclusion) are welcome.

Selected references

• J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1) (1993) 202–226. https://doi.org/10.1287/moor.18.1.202
• R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1(2) (1976) 97–116. https://doi.org/10.1287/moor.1.2.97
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• Y. Censor, S. A. Zenios, Proximal minimization algorithm with D-functions, Journal of Optimization Theory and Applications 73(3) (1992) 451–464. https://doi.org/10.1007/BF00940051
• P. Tseng, D. P. Bertsekas, On the convergence of the exponential multiplier method for convex programming, Mathematical Programming 60 (1993) 1–19. https://doi.org/10.1007/BF01580598