All missions

Motivation

Menger's theorem is the oldest of the min–max theorems of combinatorial optimization. It says that the largest number of disjoint paths joining two sets of vertices of a finite graph equals the smallest number of vertices whose removal disconnects them. The max-flow/min-cut theorem of Ford and Fulkerson (1956), the Kőnig–Egerváry theorem on bipartite matchings (1931), Whitney's characterization of $k$-connected graphs (1932) and the integrality of network-flow polytopes all belong to its family. In operations research it underlies network reliability (how many vertex failures a network survives) and disjoint routing.

Karl Menger proved it in 1927, in a paper on curves. In Zur allgemeinen Kurventheorie (Fund. Math. 10, pp. 96–115) the graph statement is a lemma, Satz δ (p. 101), on the way to characterizing the order of a point of a regular curve by the number of arcs ending there (the subject of mission II of this series).

Timeline.

• 1927. Menger states Satz β for compact regular one-dimensional spaces and proves its finite case, Satz δ, for finite unions of arcs, by induction on the number of arcs (Menger 1927).
• 1931. Kőnig observes that one step of the induction, called "offenbar" on p. 102, is in the bipartite case exactly his matching theorem, and supplies it (Kőnig 1931, see the references). Kőnig's 1936 book gives the first complete graph-theoretic proof.
• 1932. Whitney derives the two-vertex form for $k$-connected graphs.
• 1956. Ford and Fulkerson's max-flow/min-cut theorem gives the flow-theoretic proof; Dantzig and Fulkerson connect it to LP duality.

Setting

Let $G$ be a finite simple graph on a vertex set $V$, and let $P, Q \subseteq V$ be disjoint sets of vertices.

A set $S \subseteq V$ separates $P$ and $Q$ if every walk of $G$ from a vertex of $P$ to a vertex of $Q$ passes through a vertex of $S$. The set $S$ may contain vertices of $P$ and of $Q$; in particular $S = P$ always separates.

$G$ is $n$-point connected between $P$ and $Q$ ("n-punktig zusammenhängend", p. 100) if no set of fewer than $n$ vertices separates $P$ and $Q$:

$$|S| \ge n \quad\text{for every } S \text{ separating } P \text{ and } Q .$$

A family of $n$ disjoint $P$–$Q$ paths consists of paths $W_1, \dots, W_n$ of $G$, each from a vertex of $P$ to a vertex of $Q$, whose vertex sets are pairwise disjoint, end vertices included.

The degree (Grad) of $G$ is its number of edges. A part of $G$ is a spanning subgraph $H \le G$; it is proper if it lacks an edge of $G$. $G$ is irreducibly $n$-point connected between $P$ and $Q$ if it is $n$-point connected and no proper part is. For a separating set $S$, the side $K_1$ of $S$ towards $P$ is formed by the components of $G - S$ that meet $P - S$, together with their edges to $S - P$; the side $K_2$ towards $Q$ is defined symmetrically.

In Lean these are Menger27.Graphs.Separates, NPointConnected, HasDisjointPaths, IrreduciblyNPointConnected and sidePart.

Formalization targets

Goal: Satz δ (p. 101)

$$G \text{ is } n\text{-point connected between disjoint } P \text{ and } Q \quad\Longrightarrow\quad G \text{ contains } n \text{ disjoint } P\text{–}Q \text{ paths.}$$

This is the direction Menger states; the converse (disjoint paths force every separator to be large) is immediate and is not part of the mission.

Milestones: the proof of Satz δ, in the paper's order (pp. 101–102)

1. A graph $n$-point connected between $P$ and $Q$ has at least $n$ edges.
2. If it has exactly $n$ edges, it consists of $n$ disjoint $P$–$Q$ paths.
3. It contains an irreducibly $n$-point connected part $K'$.
4. If $K'$ is irreducible and has more than $n$ edges, it has a vertex $s \notin P \cup Q$ on one of its edges.
5. Through such an $s$ passes a set $S$ of exactly $n$ vertices separating $P$ and $Q$ in $K'$.
6. For an $n$-vertex separating set $S$ with $|S \cap P| = p$, the side $K_1$ is $(n-p)$-point connected between $P - S$ and $S - P$.
7. $n - p$ disjoint paths in $K_1$ and $n - q$ disjoint paths in $K_2$ (with $q = |S \cap Q|$) combine into $n$ disjoint $P$–$Q$ paths in $G$.

Significance

The result. Satz δ is the vertex form of Menger's theorem for two sets, from which the other standard forms follow: the two-vertex form, Whitney's theorem, the edge form (through line graphs), Kőnig's theorem (for bipartite $G$ with $P$, $Q$ the two sides) and, through a standard reduction, integral max-flow/min-cut for unit capacities. Menger used it as the finite step of his theorem on $n$-legs at points of regular curves.

Formalizing it. The theorem is proved, with many published proofs. Mathlib at the pinned revision has edge connectivity of simple graphs but no vertex separators between sets and no form of Menger's theorem; nothing on Prove2Me states it in set form. The mission produces a statement of Satz δ about Mathlib's SimpleGraph, together with the intermediate claims of Menger's own induction, so that the original argument, including the step Kőnig completed, can be checked. Related posed items on the platform are the two-vertex Whitney theorem Balinski61.Whitney.whitney_theorem (internally disjoint paths between two vertices) and Kőnig's theorem MatousekLP.Integrality.konig; neither is the set form stated here, and neither is proved yet.

Difficulty

The obvious argument, choosing disjoint paths one at a time, fails: a first path chosen badly can block every completion, so the paths must be chosen together. Menger's induction avoids this by passing to an irreducible part and cutting it at an $n$-vertex separator, but it needs a vertex outside $P \cup Q$ to cut at (milestone 4). When every vertex of the irreducible part lies in $P \cup Q$ the part is bipartite between $P$ and $Q$, and the claim is then Kőnig's matching theorem rather than an observation; this is the gap of 1927. The gluing step (milestone 7) is also more delicate than on the page: the paths of the two sides must meet the separator only at their ends, which depends on how the sides are cut out.

Formalization scope

Representation. Menger's gewöhnlich eindimensionaler Raum, a finite union of arcs meeting at most in end points, is read as a finite simple graph G : SimpleGraph V with [Fintype V]; $P$ and $Q$ are Finset V. Vertices are the points of $P \cup Q$ and the end and branch points (Menger's punktförmige Stücke); edges are the arcs between them, subdivided so that there are no loops or parallel edges. Subdivision changes neither separation nor the number of disjoint paths, and a separating point inside an arc can be moved to an end of the arc. Menger's degree (the number of arcs between consecutive punktförmige Stücke) becomes the number of edges, which a subdivision only increases; every milestone stays true.

Conventions and explicit readings of the paper's phrases.

• Separation is phrased through walks: every walk from $P$ to $Q$ meets $S$. Separators may meet $P$ and $Q$.
• Disjointness of $P$ and $Q$ ("fremden", p. 100) is a hypothesis of every theorem, not part of the definition. Paths are disjoint including their end points; with $P \cap Q = \emptyset$ every path has an edge.
• "Teil" is a spanning subgraph H ≤ G; "echter Teil" is H < G.
• "Offenbar enthält K′ ein punktförmiges Stück s …" (p. 102) is read as: a vertex $s \notin P \cup Q$ lying on an edge of $K'$.
• "In K′ − s sind n − 1 Punkte … so dass … S = {s, s₂, … sₙ}" is read as: a separating set of exactly $n$ vertices containing $s$.
• "Besteht aus n Bögen" (milestone 2) is read as: $n$ disjoint $P$–$Q$ paths covering every edge.
• The side $K_1$ is constructed from $G$, $P$ and $S$ (sidePart G P S), not quantified over; it has no edges at the vertices of $S \cap P$, matching Menger's $K_1 \subseteq K' - S$ considered between $P - S\cdot P$ and $S - S\cdot P$.
• The subtractions $n - p$ and $n - q$ are exact, since $|S| = n$.
• On p. 101 the induction hypothesis is printed as "Satz γ"; it is Satz δ.

Trivializations ruled out. Forcing separators to avoid $P \cup Q$, counting internally disjoint or edge-disjoint paths, or allowing two paths to share an end vertex would each change the theorem; none is done. No hypothesis restricts $n$, and $n = 0$ is the trivial case, not an excluded one.

Needed infrastructure. Walk surgery (prefixes up to the first visit of a set, concatenation, conversion of walks to paths), transfer of walks along SimpleGraph inclusions, and well-founded induction on the number of edges. Separators and disjoint path families between sets are reusable beyond this mission, for Whitney's theorem, Kőnig's theorem and flow integrality. Proofs by any method are welcome, including a proof of the goal through max-flow/min-cut or an independent argument (Göring's) bypassing the milestones.

Selected references

• K. Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115
• D. Kőnig, Gráfok és mátrixok, Matematikai és Fizikai Lapok 38 (1931), 116–119 (no DOI; English discussion in Diestel, Graph Theory, §2.1 and §3.3).
• H. Whitney, Congruent graphs and the connectivity of graphs, American Journal of Mathematics 54 (1932), 150–168. https://doi.org/10.2307/2371086
• L. R. Ford, 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
• F. Göring, Short proof of Menger's theorem, Discrete Mathematics 219 (2000), 295–296. https://doi.org/10.1016/S0012-365X(00)00088-1
• R. Diestel, Graph Theory, 5th ed., Springer, 2017, §3.3. https://doi.org/10.1007/978-3-662-53622-3

Why this formulation matters

The traveling salesman problem asks for a shortest closed route through a set of cities. Writing it as an integer program requires linear constraints whose integer solutions are exactly the routes. The assignment constraints (each city entered once and left once) are not enough: their integer solutions include collections of disjoint cycles, called subtours, that never pass through the starting city. Some extra family of constraints must rule these out.

In 1960 C. E. Miller, A. W. Tucker and R. A. Zemlin gave such a family using one auxiliary real variable per city (J. ACM 7(4), 326–329). Their MTZ constraints have polynomially many rows, $n^2-n$ for $n$ cities, whereas the subtour elimination constraints of Dantzig, Fulkerson and Johnson (1954) (Oper. Res. 2(4)) have one row per subset of cities. They also handle a generalization: a salesman who returns to base several times, visiting at most $p$ cities per trip. This is the basic form of a capacitated vehicle routing problem. MTZ-type constraints remain standard in vehicle routing models and in textbook formulations of the TSP. Their linear relaxations are known to be weaker than those of the subtour elimination formulation (Padberg and Sung, 1991).

The paper attributes the model to Tucker and reports five machine experiments with Gomory's all-integer algorithm. The computational part is outside this mission.

Setting

There are $n$ cities $1,\dots,n$ and a base city $0$. A tour is a succession of visits to cities without stopping at city $0$. In problem (1) the salesman leaves $0$, visits each of the $n$ cities exactly once and returns to $0$, possibly several times, with at most $p$ cities per tour. Formally, an itinerary is a list $I=(T_1,\dots,T_t)$ of tours. Each tour is a nonempty list of cities other than $0$ of length at most $p$, and each city $1,\dots,n$ occurs exactly once in the concatenation of the tours. The number $t$ of tours is the number of returns to $0$. Tour $(c_1,\dots,c_k)$ travels the arcs $(0,c_1),(c_1,c_2),\dots,(c_k,0)$. $a_{ij}(I)$ denotes the number of times $I$ travels the arc $(i,j)$. For real distances $d_{ij}$, the length of $I$ is the sum of $d_{ij}$ over the arcs it travels.

Problem (2) has non-negative integer variables $x_{ij}$ ($0\le i\ne j\le n$) and real variables $u_1,\dots,u_n$:

$$\min \sum\sum_{0\le i\ne j\le n} d_{ij}x_{ij}\quad\text{s.t.}\quad \sum_{\substack{i=0\\ i\ne j}}^{n} x_{ij}=1\ (j\ge1),\quad \sum_{\substack{j=0\\ j\ne i}}^{n} x_{ij}=1\ (i\ge1),\quad u_i-u_j+p\,x_{ij}\le p-1\ (1\le i\ne j\le n).$$

When the number of tours $t$ is fixed, the relation $\sum_{i=1}^n x_{i0}=t$ is added. With $t=1$ and $p\ge n$, (1) is the standard traveling salesman problem.

Formalization targets

Goal: the equivalence of (1) and (2)

For every $n\ge0$ and every $p\ge1$:

$$\{\,x : \exists u,\ (x,u)\ \text{feasible for (2)}\,\} \;=\; \{\,a(I) : I \text{ a legitimate itinerary of (1)}\,\},$$

with $\sum_{i=1}^n x_{i0}$ equal to the number of tours $t(I)$, and with the $u_i$ in the converse taken to be non-negative integers. In addition, $\sum\sum_{i\ne j} d_{ij}\,a_{ij}(I)$ equals the length of $I$ for all real $d$. The paper says that (2) "will be shown to be equivalent to (1)". Its "burden of proof" is that the two feasible sets correspond and the two objectives agree, and the goal states exactly that.

Milestones, in the order of the paper's proof

1. The constraints of (2) force $x_{ij}\in\{0,1\}$ (p. 327).
2. Along a path $r_0,\dots,r_m$ of non-base cities with all $x_{r_kr_{k+1}}=1$, $u_{r_0}-u_{r_m}\le-m$ (p. 328).
3. A feasible $x$ has no cycle that avoids city $0$, so all tours include city 0 (pp. 327–328).
4. For $p\ge1$, no tour of a feasible $x$ visits more than $p$ cities (p. 328).
5. The converse: $u_i=$ the position of city $i$ in its tour makes $(a(I),u)$ feasible, with $1\le u_i\le p$ (p. 328).
6. Under $x=a(I)$ the objective of (2) is the distance travelled in (1) (p. 327).
7. An itinerary with $t$ tours of at most $p$ cities requires $tp\ge n$ (p. 326).

Significance

The result. The theorem justifies using (2) in place of (1). Because the feasible sets match and the objectives agree, an optimal solution of (2) is an optimal itinerary of (1), and the same holds with the number of tours fixed. It also shows that a compact, polynomial-size family of linear inequalities in auxiliary potentials excludes every subtour. The same idea, with the $u_i$ read as loads or arrival times, underlies the standard capacity and time-window constraints of vehicle routing.

Formalizing it. The result is classical and its proof is short, but the paper argues informally. It follows successor chains, treats "a tour" without defining an itinerary, and leaves several steps implicit, including the hypothesis $p\ge1$ and the distinctness of $r_{p+1}$ and $r_1$. No machine-checked statement of the MTZ equivalence is recorded on the platform. The remaining work is the whole formal proof: the combinatorics that turns a 0/1 matrix with unit row and column sums and no subtours into a list of tours, the converse labelling, and the bookkeeping identity between the two objectives.

Difficulty

The inequalities themselves are elementary. Each milestone about (2) is a short computation with the potentials $u_i$. The work is in the passage from a feasible matrix $x$ to an itinerary. The successor walk from city $0$ must be shown to terminate at $0$ and to cover every arc of $x$. The resulting tours must be listed so that their arc counts reproduce $x$ exactly, including the number of arcs leaving $0$. That number is not constrained directly in (2). It equals $\sum_{i}x_{i0}$ only through a counting argument on the row and column sums. A proof that only shows some itinerary exists does not establish the correspondence the paper claims.

Formalization scope

Cities are Fin (n + 1) with 0 the base city, which is the paper's indexing. The commitments, each also stated in the items' Formalization Notes, are:

• An itinerary is a List of tours, each tour a List of cities. The paper's "legitimate itinerary" is read as: every tour nonempty, free of 0, of length at most $p$; the concatenation duplicate-free; every city $1,\dots,n$ present.
• "A feasible solution to (2) has $x_{ij}$ which do define a legitimate itinerary" is read as $x=a(I)$, the arc counts of $I$, together with $\sum_{i=1}^n x_{i0}=t(I)$ ("The number of returns to city 0 is given by $\sum x_{i0}$"). Arc counts are counts, so $x_{ij}\in\{0,1\}$ is a theorem, not an encoding choice.
• "Together with appropriate $u_i$" is made explicit as the existence of natural-number $u_i$, following the paper's remark that the $u_i$ may be taken non-negative integers. The labelling $u_i=j$ is a definition.
• Problem (2) has no variables $x_{ii}$. The matrix $x$ is indexed by all pairs and the clause $x_{ii}=0$ encodes their absence. $u_0$ exists in the encoding but appears in no constraint.
• $x_{ij}\in\mathbb N$ ("non-negative integers"), $u_i\in\mathbb R$ ("arbitrary real numbers"), and $p-1$ and $p\,x_{ij}$ are computed in $\mathbb R$.
• Added hypothesis $p\ge1$ in the goal and in milestone 4. The paper does not state it, and the claim is false without it: for $n=1$, $p=0$, $x_{01}=x_{10}=1$ is feasible for (2) but no itinerary exists.
• The distances $d_{ij}$ are arbitrary reals, with no sign, symmetry or triangle condition, as on the page.
• Milestone 2 states the exact summed bound $-m$. The page prints the weaker $j+1-k$.
• Milestone 3 excludes every cycle of $x$ avoiding $0$. The page argues for the cycle met while following successors from $0$, by an argument that applies to any such cycle.

Not formalized: the constraint and variable counts and the elimination of $x_{i0},x_{0j}$ "to produce an equivalent problem with $n^2+n$ inequalities and $n^2$ variables" (p. 328), which the paper does not make precise, and the machine experiments (pp. 328–329).

Trivializing readings are ruled out. The goal identifies $x$ with the arc counts of an itinerary, not merely the existence of some itinerary. The hypotheses are satisfiable: for $n=3$, $p=2$, the itinerary $[[1,2],[3]]$ with $u=(1,2,1)$ is feasible for (2), while the subtour $x_{01}=x_{10}=x_{23}=x_{32}=1$ is not, for any $u$. Contributions welcome: proofs of the milestones, a reusable library of "functional digraph with unit in- and out-degree" decompositions, and the optimization corollary (equal optimal values of (1) and (2)).

Selected references

• C. E. Miller, A. W. Tucker, R. A. Zemlin, Integer Programming Formulation of Traveling Salesman Problems, Journal of the ACM 7(4), 326–329, 1960. https://doi.org/10.1145/321043.321046
• G. Dantzig, R. Fulkerson, S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 393–410, 1954. https://doi.org/10.1287/opre.2.4.393
• M. Padberg, T.-Y. Sung, An analytical comparison of different formulations of the travelling salesman problem, Mathematical Programming 52, 315–357, 1991. https://doi.org/10.1007/BF01582894
• R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bulletin of the AMS 64(5), 275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4

Motivation

The proximal point algorithm is a basic iterative scheme of convex optimization and monotone operator theory. To solve a problem governed by a monotone operator, it replaces the problem by a sequence of better-conditioned problems, each regularized by a quadratic term centred at the previous iterate. Augmented Lagrangian methods, the Douglas–Rachford and ADMM splitting schemes, and many bundle methods can all be read as instances of it.

The scheme first appeared in a five-page note by Bernard Martinet in the Revue française d'informatique et de recherche opérationnelle (1970), under the name régularisation par approximations successives. Martinet stated it for a monotone variational inequality on a bounded closed convex subset of a Hilbert space and proved that the weak cluster points of the iterates are solutions. This mission formalizes that first convergence theorem as it was originally stated.

Timeline.

• 1966–1967: Hartman–Stampacchia and Lions–Stampacchia prove existence of solutions for monotone, hemicontinuous variational inequalities on bounded closed convex sets (Lions–Stampacchia 1967). Minty's lemma characterizes the solution set by the inequality with the operator evaluated at the variable point.
• 1970: Martinet introduces the regularization iteration (2) and proves Théorème 1 below (Martinet 1970). In §IV of the same note he states the convex-minimization version.
• 1976: Rockafellar extends the method to maximal monotone operators, allowing inexact steps and variable step sizes, and proves weak convergence of the whole sequence when a zero exists (Rockafellar 1976).
• 1991: Güler constructs an example in which the iterates converge weakly but not strongly (Güler 1991).

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $H'$ be its dual, and write $(\varphi, y)$ for the value of a functional $\varphi\in H'$ at $y\in H$. Let $C\subseteq H$ be convex, closed and bounded, and let $T:H\to H'$ be

• monotone on $C$: $(Tx-Ty,\,x-y)\ge0$ for all $x,y\in C$;
• hemicontinuous on $C$: for all $x,y\in C$, the map $t\mapsto T((1-t)x+ty)$, $t\in[0,1]$, is continuous into $H'$ with its weak topology.

The variational inequality (1) asks for $\bar x\in C$ such that

$$(T\bar x,\, x-\bar x)\ge 0\qquad\forall x\in C .$$

Its solution set is denoted $M$ (solSet T C in Lean).

Martinet's regularization algorithm starts from $x^0\in C$. Given $x^n\in C$, it determines $x^{n+1}\in C$ such that

$$(Tx^{n+1},\, x-x^{n+1})+\langle x^{n+1}-x^n,\, x-x^{n+1}\rangle\ge 0\qquad\forall x\in C. \tag{2}$$

In words, $x^{n+1}$ solves the variational inequality for the operator $T+(\,\cdot\,-x^n)$, which is strongly monotone. A point $\tilde x$ is a weak cluster point of $(x^n)$ if every neighbourhood of $\tilde x$ in the weak topology contains $x^n$ for infinitely many $n$.

Formalization targets

Goal: Théorème 1

$$\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in M .$$

Every weak cluster point of the regularized iterates solves (1). The paper's Lemme 2 states the same thing. The goal assumes neither that (1) has a solution nor that $T$ is bounded on $C$.

Milestones, in the order the paper uses them

1. §2.1: (1) has at least one solution when $C\neq\emptyset$, so $M\neq\emptyset$.
2. §2.2: the step (2) has exactly one solution $x^{n+1}\in C$ for every $x^n\in C$.
3. §2.3, (5): Minty's characterization $M=\{\bar x\in C\mid (Tx,\,x-\bar x)\ge0\ \forall x\in C\}$.
4. §2.3, (7): for every $\bar x\in M$, $\|x^{n+1}-\bar x\|^2\le\|x^n-\bar x\|^2-\|x^{n+1}-x^n\|^2$.
5. Lemme 1: $\|x^{n+1}-x^n\|\to0$.
6. §2.3, (8): $\liminf_n (Tx^{n+1},\,x-x^{n+1})\ge0$ for every $x\in C$.
7. §2.3, (9): $\liminf_n (Tx,\,x-x^{n})\ge0$ for every $x\in C$.
8. Corollaire (stronger than the goal): if $M=\{\bar x\}$, then $x^n\rightharpoonup\bar x$.

Significance

The result. Théorème 1 is the first convergence theorem for the proximal point method. The method only needs to solve strongly monotone subproblems, and those are well posed even when the original problem is not. Together with the existence result, the theorem says the iterates accumulate weakly only at solutions. When the solution is unique, the whole sequence converges weakly (the Corollaire). The later theory of Rockafellar, Brézis–Lions and the splitting literature refines this statement.

Formalizing it. The result has been proved since 1970. What this mission adds is a machine-checked version that follows the original hypotheses: an operator into the dual, hemicontinuity rather than continuity, and no maximality assumption. The cited ingredients, the Lions–Stampacchia existence theorem in an infinite-dimensional Hilbert space and Minty's lemma, are not in Mathlib as far as this mission is aware. Formalizing them is part of the work and is reusable well beyond this paper. The milestone items on the platform are statements awaiting proof. None of them has a machine-checked proof yet.

Difficulty

Lemme 1 and inequality (7) follow from the defining inequality (2) and the algebra of the inner product. The difficulty is at two other points.

First, the iterates satisfy the variational inequality only approximately, and only with $T$ evaluated at the iterate. A weak cluster point gives no control over $Tx^{n}$, because $T$ is merely hemicontinuous and is not assumed weakly continuous or bounded. The obvious idea, to pass to the limit in $(Tx^{n+1},\,x-x^{n+1})\ge -\varepsilon_n$, fails for this reason. Passing to the limit requires the reformulation in which $T$ is evaluated at a fixed point of $C$. That reformulation is Minty's characterization (5), and proving it uses hemicontinuity along segments.

Second, the proof of Lemme 1 needs a solution of (1) to exist. In infinite dimensions that is the Lions–Stampacchia theorem. Its standard proof goes through Brouwer's fixed point theorem on finite-dimensional sections together with weak compactness of $C$, and this is the heaviest item of the mission.

Formalization scope

• $H$ is a real Hilbert space: NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H. The paper says only "espace de Hilbert". Its ordered inequalities force real scalars.
• $H'$ is StrongDual ℝ H, and $(\varphi,y)$ is φ y. $T$ is not replaced by a map $H\to H$ through the Riesz isomorphism.
• Hemicontinuity is weak-* continuity: for $x,y\in C$ and every $z\in H$, the map $t\mapsto (T((1-t)x+ty),z)$ is continuous on $[0,1]$. Since $H$ is reflexive, this is the paper's weak topology on $H'$. It is not strengthened to continuity of $T$.
• The algorithm is a relation (IsRegSeq): any sequence with $x^0\in C$ that satisfies (2) at every step. Existence and uniqueness of the step are milestone 2, not built into a definition.
• A weak cluster point is MapClusterPt in WeakSpace ℝ H, a cluster point in the weak topology. It is not a cluster point in the norm topology, which would make the goal weaker.
• $\liminf_n a_n\ge0$ in (8) and (9) is stated as $\forall\varepsilon>0$, eventually $a_n\ge-\varepsilon$. Filter.liminf on $\mathbb R$ returns a junk value on sequences that are unbounded below.
• "C nonempty" is added to the existence milestone. The paper leaves it implicit, and the claim is false for $C=\emptyset$.
• In Lean the sequence is called $x$ and an arbitrary point of $C$ is called $y$. The paper uses the letter $x$ for both.

A trivializing formalization is ruled out. The goal does not assume $M\neq\emptyset$, boundedness of $T$, or strong cluster points. Its hypotheses are satisfiable: $H=\mathbb R$, $C=[-1,1]$, $(Tx,y)=xy$, $x^n=2^{-n}$ is an instance, checked locally.

Not formalized: Remarques 1 and 2 of §II (a variable-weight variant of (2), whose printed form is apparently misprinted, and the removal of boundedness of $C$ under a coercivity condition), because the paper gives neither a proof. Théorème 2 (§III) and the convex-minimization §IV are not formalized either. §IV is the subject of the companion mission.

Contributions are welcome on each milestone, and especially on the general infrastructure: Minty's lemma, Hartman–Stampacchia/Lions–Stampacchia existence for monotone hemicontinuous operators, and the fact that bounded sequences in a Hilbert space have weak cluster points. A proved Brouwer fixed point theorem (AGT.brouwer_fixed_point) and a Banach–Alaoglu theorem (FamousTheorems.banach_alaoglu) are available on the platform as tools.

Selected references

• B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3) (1970), 154–158. https://doi.org/10.1051/m2an/197004R301541
• J.-L. Lions, G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20 (1967), 493–519. https://doi.org/10.1002/cpa.3160200302
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14 (1976), 877–898. https://doi.org/10.1137/0314056
• O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29 (1991), 403–419. https://doi.org/10.1137/0329022

Motivation

Many problems in optimization and equilibrium modelling, among them linear and nonlinear complementarity problems, variational inequalities over polyhedra, and the Karush–Kuhn–Tucker conditions of nonlinear programs, can be written as a single generalized equation

$$0\in f(x)+\partial\psi_C(x),$$

where $\partial\psi_C$ is the normal-cone operator of a closed convex set $C$. S. M. Robinson introduced strong regularity of such an inclusion at a solution $x_0$ in Strongly regular generalized equations (1980) and proved an implicit-function theorem for it: when the linearised inclusion has a locally unique, Lipschitz inverse, solutions of the perturbed problem exist, are locally unique and depend Lipschitz-continuously on the perturbation. Strong regularity has since become the standard stability notion behind sensitivity analysis and the local convergence of Newton-type methods for variational problems; see Dontchev and Rockafellar, Implicit Functions and Solution Mappings (Springer, 2nd ed. 2014, doi:10.1007/978-1-4939-1037-3).

Strong regularity depends only on the linearisation, so deciding it means deciding it for a linear generalized equation. For a general polyhedral set $C$ the paper's appendix does this by a reduction: locally around $x_0$ the problem is equivalent to a homogeneous problem on a cone, the reduced form, and strong regularity is equivalent to unique solvability of that reduced form. This mission formalizes that appendix and the criterion it yields.

Setting

Work in $\mathbb R^n$ with the standard inner product, which identifies $\mathbb R^n$ with its dual. For $C\subseteq\mathbb R^n$ the normal cone at $x$ is

$$\partial\psi_C(x)=\{y:\langle y,c-x\rangle\le 0\ \text{for all } c\in C\}\ \text{if } x\in C,\qquad \partial\psi_C(x)=\emptyset\ \text{if } x\notin C.$$

A set is polyhedral convex if it is the intersection of finitely many closed half-spaces. Fix a nonempty polyhedral convex $C$, an $n\times n$ real matrix $A$ and $a\in\mathbb R^n$, and consider

$$0\in Ax+a+\partial\psi_C(x).\qquad\text{(A.1)}$$

It is strongly regular at a solution $x_0$ with constant $\lambda$ if there are neighbourhoods $U$ of $0$ and $V$ of $x_0$ such that for each $y\in U$ the perturbed inclusion

$$y\in Ax+a+\partial\psi_C(x)\qquad\text{(A.2)}$$

has exactly one solution $x=s(y)$ in $V$, and $\|s(y_1)-s(y_2)\|\le\lambda\|y_1-y_2\|$ on $U$.

The reduction uses the following objects, all built from the data:

• $y_0:=Ax_0+a$;
• the face $F:=\partial\psi_C^*(-y_0)$, the set of maximisers of $\langle -y_0,\cdot\rangle$ over $C$ (it contains $x_0$);
• the tangent cone $T:=T_F(x_0)=\partial\psi_F(x_0)^\circ$, the polar of the normal cone of $F$ at $x_0$;
• the subspace $L$ parallel to $F$ (the direction of its affine hull) and the orthogonal projector $P_L$;
• the lineality space $M$ of $T$, the subspace $L\cap M^\perp$, and the cone $K:=T\cap M^\perp$.

The reduced form of (A.1) at $x_0$ is the inclusion $z\in P_LAw+\partial\psi_T(w)$ for $z\in L$; in an orthonormal basis adapted to $M$, $L\cap M^\perp$ and $L^\perp$ it is $z\in Bw+\partial\psi_{\mathbb R^r\times K}(w)$ with an $(r+s)\times(r+s)$ matrix $B$. It is vacuous when $L=\{0\}$.

Formalization targets

Goal: Theorem A.4 (p. 60)

If $x_0$ solves (A.1), then (A.1) is strongly regular at $x_0$ if and only if

$$L=\{0\}\quad\text{or}\quad\forall z\in L\ \exists!\,w\in\mathbb R^n:\ z\in P_LAw+\partial\psi_T(w).$$

No Lipschitz constant is fixed: the left side is "strongly regular for some $\lambda$".

Milestones

1. Proposition A.1 (p. 58): for $x_0\in C$, $(C-x_0)\cap U=T_C(x_0)\cap U$ for some neighbourhood $U$ of $0$.
2. Proposition A.2 (p. 58): on $F=\partial\psi_C^*(-y_0)$, $\partial\psi_F(x)=\partial\psi_C(x)+y_0\mathbb R_+$, and $\partial\psi_C^*(-y)\subset F$ for $y$ near $y_0$.
3. Proposition A.3 (p. 58): for $x_0\in F$, near the origin, $0\in(y_0+k)+\partial\psi_C(x_0+h)$ iff $0\in P_Lk+\partial\psi_T(h)$.
4. The correspondence (A.4) (p. 60): for $x$ near $x_0$ and small $y$, (A.2) holds iff $0\in P_L(Ah-y)+\partial\psi_T(h)$ with $h=x-x_0$.

Companions

• Corollary 3.2 (p. 53), in two items. Sufficiency: the reduced form is vacuous, or $B_{11}$ is nonsingular and the Schur complement $B/B_{11}$ is positive definite. Characterisation when $K=\mathbb R^s_+$: strongly regular iff vacuous, or $B_{11}$ nonsingular and $B/B_{11}$ a P-matrix.
• The 3 × 3 linear complementarity example of §4 (p. 53): strongly regular at $x_0=(1,0,0)$, and not strongly regular once the entry $5$ of $A$ becomes $4$.

Significance

Theorem A.4 turns a local stability property, defined through neighbourhoods and an inverse map, into a finite-dimensional algebraic question about one homogeneous problem on a polyhedral cone. Combined with the Schur-complement criterion of Theorem 3.1, it gives checkable conditions (Corollary 3.2): nonsingularity of a block and positive definiteness, or the P-matrix property, of its Schur complement. Through the KKT reformulation of §4 this is the route by which strong second-order sufficiency and linear independence of binding constraint gradients imply strong regularity in nonlinear programming. The example of p. 53 shows the criterion deciding cases where $A$ itself is neither positive definite nor a P-matrix.

The results are classical and proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a coordinate-free statement of the reduced form, which the paper writes only in an adapted basis; a Lean account of exposed faces and tangent cones of polyhedra, with their local conic structure (Propositions A.1–A.2), which the paper lists "without proof" and cites to Rockafellar; and checked versions of the corollary and the example.

Difficulty

The definition of strong regularity is local, while condition (ii) is global on $L$. The obvious argument, "linearise and read off the inverse", does not apply, because $\partial\psi_C$ is a set-valued map whose graph changes shape from point to point. The step that carries the weight is Proposition A.3: a perturbation of $y_0$ may move the solution off the face $F$, and only polyhedrality, through the finitely many values of $\partial\psi_C$ on $F$ and the local conic structure of A.1–A.2, rules this out uniformly in a neighbourhood. The direction from strong regularity to (ii) needs positive homogeneity of the reduced form to pass from uniqueness near $0$ to uniqueness on all of $L$. The direction from (ii) to strong regularity needs the Lipschitz property of a single-valued inverse of a polyhedral multifunction (Robinson 1979, cited as [12, Proposition 2]), which is not elementary.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n), with inclusions written as memberships: (A.2) is $y-(Ax+a)\in\partial\psi_C(x)$. A matrix acts through Matrix.toEuclideanLin. The normal cone carries the clause $x\in C$, so $\partial\psi_C(x)=\emptyset$ off $C$; without it every inclusion would be satisfiable at points outside $C$ and the statements would change meaning.
• $T_C(x_0)$ is the polar of the normal cone, as on p. 58, not the closure of the cone of feasible directions. $F$ is the set of maximisers of $\langle -y_0,\cdot\rangle$ (the sign matters: the opposite face would make the theorem false). $L$ is the direction of the affine span of $F$, and $P_L$ is Mathlib's Submodule.starProjection.
• The reduced form is stated basis-free on $L$; $\partial\psi_T$ is the normal cone of $T$ in all of $\mathbb R^n$. In Corollary 3.2, $B_{11}$ and $B/B_{11}$ are expressed through projectors onto $M$ and $L\cap M^\perp$. Only the case $K=\mathbb R^s_+$ is stated in a basis, an orthonormal basis of $L\cap M^\perp$ in which $K$ is the orthant.
• "Positive definite" does not require symmetry. "Strongly regular" without a constant is existential in $\lambda$, with $\lambda$ real.
• Corollary 3.2's second sentence refers on the page to "(3.8)", an evident slip for (3.9); it is formalized for (3.9).
• The standing assumption "C nonempty polyhedral convex" is a hypothesis of every item.
• A trivializing formalization is ruled out: strong regularity requires existence, uniqueness in $V$ and the Lipschitz bound together, and condition (ii) requires existence and uniqueness for every $z\in L$.
• Needed infrastructure: faces and tangent cones of polyhedra and their local structure (Minkowski–Weyl, finitely many faces), orthogonal decompositions, and Lipschitz continuity of single-valued polyhedral inverses. All of this is reusable beyond this mission. Proofs of the propositions, of the correspondence, and of the companions are welcome independently.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1), 43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• S. M. Robinson, Generalized equations and their solutions, Part I: Basic theory, Mathematical Programming Study 10, 128–141, 1979. https://doi.org/10.1007/BFb0120850
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3
• R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8, 189–211, 1974. https://doi.org/10.1016/0024-3795(74)90066-4

Motivation

A constrained system can be written as a generalized equation: a smooth or linear expression must balance the normal cone of a feasible set. This form includes variational inequalities and the first-order conditions of many optimization problems. It is useful to know whether a small change in the right-hand side determines one nearby solution and how far that solution moves. In the linear finite-dimensional case, Robinson's Theorem 3.1 gives matrix conditions that guarantee something stronger: a unique solution for every right-hand side, with one Lipschitz bound valid over the entire space. The theorem also identifies an exact matrix criterion when the feasible set is a product with a nonnegative orthant.

The question is relevant whenever some coordinates of a system are free and others are constrained by inequalities. Eliminating the free coordinates produces a smaller matrix, the Schur complement. The resulting condition can be checked on the reduced block, and in the orthant case it becomes the familiar P-matrix criterion from linear complementarity. Robinson states both claims in a single theorem and relates them to the behavior of a generalized equation rather than to an isolated matrix property Robinson, pp. 51–52.

Setting

Let $r,s$ be positive integers and give $\mathbb R^{r+s}$ its Euclidean norm. Write $w=(w_1,w_2)$, with $w_1\in\mathbb R^r$ and $w_2\in\mathbb R^s$. Let $K\subseteq\mathbb R^s$ be nonempty, closed, and convex, and put $D=\mathbb R^r\times K$. For $w\in D$, the normal cone is

$$N_D(w)=\{v\in\mathbb R^{r+s}:\langle v,c-w\rangle\leq0\text{ for every }c\in D\}.$$

For $w\notin D$, $N_D(w)$ is empty. Thus the inclusion $y\in Aw+N_D(w)$ itself enforces feasibility. This is Robinson's indicator-subdifferential convention Robinson, pp. 43 and 51.

Partition the real square matrix $A$ into blocks $A_{11}$, $A_{12}$, $A_{21}$, and $A_{22}$, where $A_{11}$ is $r\times r$. When $A_{11}$ is nonsingular, its Schur complement in $A$ is

$$A/A_{11}=A_{22}-A_{21}A_{11}^{-1}A_{12}.$$

A real matrix $M$ is positive definite in the theorem's sense when $v^\top Mv>0$ for every nonzero $v$. Symmetry is not assumed. A P-matrix has strictly positive determinants for every nonempty principal submatrix. Write $\mathbb R^s_+$ for the vectors with all components nonnegative. These conventions are stated or used in Theorem 3.1 and its proof.

Formalization targets

General closed convex set

For $T_K(w)=Aw+N_{\mathbb R^r\times K}(w)$, the first target is the sufficient condition

$$\det A_{11}\ne0\quad\text{and}\quad v^\top(A/A_{11})v>0\;(v\ne0) \quad\Longrightarrow\quad T_K^{-1}:\mathbb R^{r+s}\to\mathbb R^{r+s}\text{ is Lipschitz}.$$

Here “is Lipschitz” includes that exactly one inverse value exists at every $y$. The assertion holds for every nonempty closed convex $K$; it is not restricted to polyhedral sets.

Nonnegative orthant

When $K=\mathbb R^s_+$, the second target is an equivalence:

$$T_{\mathbb R^s_+}^{-1}\text{ is everywhere defined, single-valued and Lipschitz} \quad\Longleftrightarrow\quad \det A_{11}\ne0\text{ and }A/A_{11}\text{ is a P-matrix}.$$

The goal theorem is the conjunction of these two statements, matching Theorem 3.1. Its milestones record the paper's local upper Lipschitz assertion for polyhedral multifunctions, the block reduction, the reduced inverse result, the complementarity characterization, and the necessity of nonsingularity.

Significance

The first part gives a global sensitivity guarantee for a generalized equation with an arbitrary nonempty closed convex lower-block constraint. For any two right-hand sides, their unique solutions differ by at most a fixed multiple of the distance between those right-hand sides. The second part tells when this guarantee holds for the orthant model: the P-matrix condition is necessary as well as sufficient. These are the precise conclusions of Robinson's theorem; the mission concerns their machine-checked formalization, not an unresolved mathematical conjecture.

A complete development would provide reusable definitions of the normal-cone generalized equation, an explicitly nonsymmetric notion of positive definiteness, P-matrices, and the global inverse property. It would also formalize the linear complementarity characterization quoted in the paper. The current draft has Lean-checked statements with proof placeholders. No proof of Theorem 3.1 or of its milestones is claimed here.

Difficulty

Nonsingularity of the full matrix $A$ alone does not decide whether the constrained inverse exists uniquely: the normal cone can change as $w_2$ reaches different faces of $K$. A pointwise uniqueness argument also does not by itself supply one Lipschitz constant on all of $\mathbb R^{r+s}$. For the orthant case, checking only the full determinant or leading principal minors would miss the criterion Robinson invokes; every nonempty principal minor matters. The difficulty is to connect a global statement about all right-hand sides with the reduced matrix condition while preserving the normal cone's behavior at boundary points Robinson, pp. 51–52.

Formalization scope

Lean represents $\mathbb R^{r+s}$ as a Euclidean space indexed by the disjoint union of $\mathrm{Fin}(r)$ and $\mathrm{Fin}(s)$. This gives the paper's Euclidean norm rather than the sup norm of a product type. The normal cone is empty off its set, and the inverse property explicitly requires existence for every right-hand side, uniqueness, and one global real Lipschitz bound. The Schur complement appears only with a nonsingular $A_{11}$ in the substantive claims; matrix inversion on a singular input would otherwise be totalized by Lean. Positive definiteness does not add a symmetry hypothesis. The goal retains $r,s>0$ as printed; the paper's later remark about zero-dimensional blocks is outside this theorem.

The polyhedral milestones use finite intersections of closed half-spaces. The reduced-operator milestone uses a nonempty closed convex $K$, matching the theorem's setting. The LCP milestone allows any finite dimension; at dimension zero, both its universal uniqueness statement and its empty-minor P-matrix condition hold. A weaker encoding in which the inverse is merely single-valued where it happens to exist would erase the global conclusion and is excluded here.

Solvers can contribute the block-normal-cone equivalence, the global inverse statement for the reduced operator, the polyhedral Lipschitz result, the P-matrix characterization, and the final theorem. The normal-cone and matrix definitions can also serve later generalized-equation missions that use the same conventions.

Selected references

• S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 43–62, 1980. DOI 10.1287/moor.5.1.43.

Motivation

The job-shop scheduling problem asks how to time a set of tasks on shared machines so that every product is finished as early as possible. Around 1959 several authors proposed to solve it with Gomory's then new integer programming (Gomory 1958). The obstacle is the noninterference condition: two tasks on the same machine must not overlap, so one of them must finish before the other starts. That is an "either-or" condition. It describes a nonconvex set, and classical linear programming cannot express it.

A. S. Manne's note On the Job-Shop Scheduling Problem (Operations Research 8 (1960) 219–223) writes the either-or condition as two linear inequalities in integers. It adds one 0–1 variable per pair of tasks that compete for a machine, and it uses a large constant derived from a bound $T$ on the start days. This is the origin of the big-M disjunctive formulation, which remains the standard textbook integer program for job shops and, more broadly, the standard way to linearize a disjunction of two linear inequalities.

Timeline. Johnson (1954) introduced the make-span criterion for two- and three-stage production schedules. Bowman (1959) and Wagner (1959) proposed integer programs for machine scheduling. Manne (1960), stimulated by Bowman's paper, gave the formulation stated here. He counted its unknowns as 275 for 5 machines with 10 tasks each, against 600 for Wagner's formulation on the same example (p. 222).

Setting

There are $n\ge1$ tasks and $M$ machines. Task $j$ requires the single machine $\mu(j)$ for $a_j$ consecutive days, where $a_j$ is an integer. An integer horizon $T$ bounds the start days: the integer unknown $x_j\in\{0,1,\dots,T\}$ is the day on which task $j$ begins. A pair $(j,k)$ with $j<k$ and $\mu(j)=\mu(k)$ is a conflicting pair. For each such pair the tasks must not overlap:

$$x_j-x_k\ge a_k\quad\text{or else}\quad x_k-x_j\ge a_j. \tag{1}$$

The instance may also impose precedence $x_j+a_j\le x_k$ for given pairs (5a), exact delays $x_j+a_j+\Theta_{jk}=x_k$ for given pairs (5c), and delivery dates $x_j+a_j\le d_j$ for given tasks (6). A schedule is an $x\in\{0,\dots,T\}^n$ satisfying (1), (5a), (5c) and (6). Its make-span is

$$\operatorname{ms}(x)=\max_{j}\,(x_j+a_j),$$

the calendar time needed for all jobs when the shop starts on day $0$.

Manne's integer program has integer unknowns $x_j$ with $0\le x_j\le T$, one integer $y_{jk}$ for each conflicting pair, and the minimand $t$, subject to (5a), (5c), (6),

$$0\le y_{jk}\le 1,\tag{2}$$ $$(T+a_k)\,y_{jk}+(x_j-x_k)\ge a_k,\tag{3}$$ $$(T+a_j)(1-y_{jk})+(x_k-x_j)\ge a_j,\tag{4}$$

and $x_j+a_j\le t$ for every $j$ (7). The value $y_{jk}=1$ means that $j$ precedes $k$; $y_{jk}=0$ means that $k$ precedes $j$.

Formalization targets

Goal: the integer program solves the make-span problem

For every instance and every integer $t^\ast$,

$$t^\ast=\min\{t:\ \exists\,x,y\ \text{integer satisfying } 0\le x_j\le T \text{ and } (2)\text{–}(7)\}\iff t^\ast=\min_{x\ \text{schedule}}\operatorname{ms}(x).$$

Both minima are required to exist. In particular the program has an optimum exactly when a schedule exists. The paper claims this when it says that "the problem now consists of the minimization of $t$" subject to (2)–(7) (p. 221).

Milestones

1. Pair equivalence (p. 220). If $|x_j-x_k|\le T$, some integer $y_{jk}$ satisfies (2)–(4) if and only if (1) holds.
2. Equal start days are excluded (p. 220). If $x_j=x_k$ and $a_j,a_k>0$, no $y_{jk}$ satisfies (2)–(4).
3. Feasibility correspondence (pp. 220–221). For fixed $x$ and $t$, some $y$ makes $(x,y,t)$ feasible for (2)–(7) if and only if $x$ is a schedule with $x_j+a_j\le t$ for all $j$.
4. The $y_{jk}$ must be discrete (p. 222). With $y_{jk}$ real in $[0,1]$ and $0<a_j,a_k\le T$, conditions (3)–(4) admit $x_j=x_k$, where (1) fails.
5. Counting unknowns (pp. 221–222). With $M$ machines of $p$ tasks each, $n=Mp$ and there are $M\,p(p-1)/2$ conflicting pairs; for $M=5$, $p=10$ this gives $50+225=275$ unknowns.

Significance

The result. The goal certifies that a single integer program, with one binary variable per conflicting pair, computes the optimal make-span of a job shop with precedence, exact delays and delivery dates. The same pattern is used whenever a disjunction $f\ge0$ or $g\ge0$ of bounded linear forms has to be put into a mixed-integer program: a binary variable selects the active branch, and a constant at least as large as the range of the inactive form switches the other branch off. Milestone 1 is that pattern in its simplest form, and milestone 4 shows why the binary variable cannot be relaxed.

Formalizing it. The paper's argument is informal. It rests on a summary table of admissible values of $y_{jk}$ that holds only when the gap $|x_j-x_k|$ is large enough. A machine-checked version fixes the exact hypotheses: integrality of $y_{jk}$, the bound $|x_j-x_k|\le T$, and nonemptiness of the task set. To the best of the curators' knowledge, no machine-checked proof of the correctness of the big-M job-shop formulation exists; the definitions here can serve later scheduling missions that need a disjunctive integer program.

Difficulty

The mathematics is elementary, and the difficulty lies in stating it exactly. The obvious reading, "(3)–(4) are equivalent to (1)", is false without the bound $|x_j-x_k|\le T$. For instance, with $y_{jk}=0$ condition (4) reads $x_j-x_k\le T$, which cuts off valid orders if start days may lie beyond the horizon. It is also false for real $y_{jk}$. Equally, "minimize $t$ subject to (7)" equals the maximum of $x_j+a_j$ only after the optimum over $t$ and over $x$ are interchanged and the empty task set is excluded. A naive formalization that states the schedule side as "the least $t$ with (7)" proves nothing about the make-span.

Formalization scope

Tasks are Fin n (the paper's task $j$ is index $j-1$), machines Fin M. Start days, durations, horizon, delays, delivery dates, $y_{jk}$ and $t$ are integers (ℤ), so that $x_j-x_k$ and $1-y_{jk}$ are not truncated. Durations are not assumed positive except in milestones 2 and 4, where positivity is necessary. One definitions file, ManneJobShop.Formulation.Model, holds the instance, the conflicting pairs, schedules, the make-span (Finset.sup', so $n\ge1$ is required via [NeZero n]) and the integer program.

Explicit readings of loose phrases:

• "a (large) integer $T$ that will constitute a redundant upper bound upon the unknowns $x_j$" (p. 219): both the schedule problem and the integer program restrict start days to $0\le x_j\le T$. Redundancy is not assumed.
• "The effect of conditions (3) and (4) may therefore be summarized as follows" (p. 220): stated as the equivalence of milestone 1 and the exclusion of milestone 2, not row by row (for $0<x_j-x_k<a_k$, condition (3) forces $y_{jk}=1$, not $\{0,1\}$).
• "the minimization of $t$" (p. 221): IsLeast of the feasible values of $t$, matched against IsLeast of the set of make-spans of schedules.
• "necessarily of a discrete nature" (p. 222): existence of a real $y_{jk}\in[0,1]$ satisfying (3)–(4) at $x_j=x_k$ when $0<a_j,a_k\le T$ ("large" $T$ read as $T\ge a_j,a_k$).
• "$m$ possible conflicting pairs of machine assignments" (p. 222): pairs $j<k$ on the same machine, one $y_{jk}$ each.
• "If task $j$ is the last task which the shop is to perform upon the item" (p. 221): a delivery date may be attached to any task, which contains the paper's case.

Trivializing formalizations are ruled out: the make-span is a maximum, not a restatement of (7); $y_{jk}$ is an integer; the horizon appears on both sides; the goal is stated for every instance with $n\ge1$, including infeasible ones. The (5b) example is (5a) for two pairs. Wagner's comparison, the remarks on Gomory's algorithm, Dantzig's secondary constraints and Monte Carlo methods, and the economic discussion of the make-span are not formalized. Proofs of every milestone and of the goal are welcome.

Selected references

• A. S. Manne, On the Job-Shop Scheduling Problem, Operations Research 8(2) (1960) 219–223. https://doi.org/10.1287/opre.8.2.219
• E. H. Bowman, The Schedule-Sequencing Problem, Operations Research 7(5) (1959) 621–624. https://doi.org/10.1287/opre.7.5.621
• H. M. Wagner, An Integer Linear-Programming Model for Machine Scheduling, Naval Research Logistics Quarterly 6(2) (1959) 131–140. https://doi.org/10.1002/nav.3800060205
• R. E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the AMS 64(5) (1958) 275–278. https://doi.org/10.1090/S0002-9904-1958-10224-4
• S. M. Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, Naval Research Logistics Quarterly 1(1) (1954) 61–68. https://doi.org/10.1002/nav.3800010110

Motivation

Many problems of optimization and equilibrium can be written as one inclusion. Some examples are the Karush–Kuhn–Tucker conditions of a nonlinear program, nonlinear complementarity problems, variational inequalities and the equilibrium conditions of economic and traffic models. In each of them a point $x$ has to satisfy $0 \in f(x) + \partial\psi_C(x)$. In applications the data $f$ depend on parameters: estimated coefficients, prices, or the iterate of an algorithm. One then wants to know whether a solution persists under a perturbation of the parameter, whether it stays locally unique, and how fast it moves. For a smooth equation $f(p, x) = 0$ the classical implicit-function theorem answers all three questions. Inequality constraints make the solution set nonsmooth, and the classical theorem no longer applies.

S. M. Robinson's paper Strongly regular generalized equations (Math. Oper. Res. 5 (1980) 43–62) introduced the condition of strong regularity and proved an implicit-function theorem for generalized equations under it. The condition and the theorem became the starting point of the stability theory of variational inequalities and nonlinear programs. Later work characterises strong regularity for nonlinear programs (Robinson's own §4, through the strong second-order sufficient condition), and develops it in the theory of metric regularity and of single-valued Lipschitz localisations (Dontchev–Rockafellar, Implicit Functions and Solution Mappings, Springer 2009/2014). Its sensitivity results underlie the convergence analysis of Newton and sequential quadratic programming methods for these problems.

This mission formalizes §1–§2 of the paper: the definition, the implicit-function theorem (Theorem 2.1) with its proof, and the three results derived from it.

Setting

Let $X$ be a real normed linear space and $X'$ its topological dual, the continuous linear functionals on $X$. Let $C \subseteq X$ be closed and convex. The normal-cone operator of $C$ is

$$\partial\psi_C(x) = \begin{cases} \{y \in X' : y(c - x) \le 0 \text{ for all } c \in C\}, & x \in C, \\ \emptyset, & x \notin C. \end{cases}$$

A generalized equation is the inclusion $0 \in f(x) + \partial\psi_C(x)$, for a function $f$ from an open set $\Omega \subseteq X$ to $X'$. For $C = X$ it is the equation $f(x) = 0$. For $C$ the nonnegative orthant of $\mathbb R^n$ it is the nonlinear complementarity problem. For a general closed convex $C$ it is the variational inequality over $C$.

Let $x_0 \in \Omega$ solve the generalized equation, and let $f$ be Fréchet differentiable at $x_0$. Linearising $f$ gives the multifunction

$$T x = f(x_0) + f'(x_0)(x - x_0) + \partial\psi_C(x).$$

The generalized equation is strongly regular at $x_0$ with associated Lipschitz constant $\lambda$ if there are neighbourhoods $U$ of $0$ in $X'$ and $V$ of $x_0$ with the following property: for every $y \in U$ the inclusion $y \in Tx$ has exactly one solution $s(y)$ in $V$, and $\|s(y_1) - s(y_2)\| \le \lambda \|y_1 - y_2\|$ on $U$. The condition depends only on $f(x_0)$, $f'(x_0)$ and $C$.

In the parametric problem the function is $f(p, x)$, with $p$ in a topological space $P$ and base point $p_0$. Its partial derivative in $x$ is $f'(p, x)$.

Formalization targets

Goal: Theorem 2.1 (p. 45)

Assume that $f'$ exists on $P \times \Omega$, that $f$ and $f'$ are continuous at $(p_0, x_0)$, and that $x_0$ solves $0 \in f(p_0, x) + \partial\psi_C(x)$, strongly regularly with constant $\lambda$. Then for every $\varepsilon > 0$ there are neighbourhoods $N_\varepsilon$ of $p_0$ and $W_\varepsilon$ of $x_0$, and a function $x : N_\varepsilon \to W_\varepsilon$, with two properties. First, $x(p)$ is the unique solution in $W_\varepsilon$ of $0 \in f(p, x) + \partial\psi_C(x)$. Second,

$$\|x(p) - x(q)\| \le (\lambda + \varepsilon)\,\|f(p, x(q)) - f(q, x(q))\| \qquad (p, q \in N_\varepsilon).$$

Milestones: the steps of the proof (p. 46)

Write $L$ for the linearisation at $(p_0, x_0)$, $r(p, x) = f(p_0, x_0) + f'(p_0, x_0)(x - x_0) - f(p, x)$ for the residual, and $\Phi_p(x) = V \cap L^{-1}[r(p, x)]$. The milestones are four claims of the proof:

1. On the closed ball $V_\varepsilon$, the fixed points of $\Phi_p$ are exactly the solutions of the perturbed inclusion.
2. $\|\Phi_p(x_1) - \Phi_p(x_2)\| \le \lambda\delta \|x_1 - x_2\|$ on $V_\varepsilon$.
3. $\Phi_p$ maps $V_\varepsilon$ into itself.
4. The contraction principle on $V_\varepsilon$, with the bound $\|x(p) - x\| \le (1 - \lambda\delta)^{-1} \|\Phi_p(x) - x\|$ (2.5).

Companion results

• Corollary 2.2 (pp. 46–47). If $P$ lies in a normed space and $\|f(p, x) - f(q, x)\| \le \nu \|p - q\|$, then $x(\cdot)$ is Lipschitzian with modulus $\nu(\lambda + \varepsilon)$.
• Theorem 2.3 (p. 47). Let $\Phi_p(x_0)$ be the unique local solution of the linear generalized equation $0 \in f(p, x_0) + f'(p_0, x_0)(x - x_0) + \partial\psi_C(x)$. Then $\|x(p) - \Phi_p(x_0)\| \le \alpha_\varepsilon(p)\|p - p_0\|$, with $\alpha_\varepsilon(p) \to 0$.
• Theorem 2.4 (p. 48). This is a perturbation lemma for linear generalized equations $0 \in Ax + a + \partial\psi_C(x)$. Near $(A_0, a_0)$ the localised inverse stays single-valued, and it is Lipschitzian with modulus $\lambda(1 - \lambda\|A - A_0\|)^{-1}$.
• The case $C = X$ (remark on p. 45). There strong regularity is equivalent to $f'(x_0)$ having a continuous linear inverse.
• Strong regularity is the weakest possible condition (remark on p. 47). For the canonical perturbation $f(p,x) = f(x_0) + f'(x_0)(x - x_0) - p$, $p \in X'$, locally unique solvability with a Lipschitzian solution map $x(\cdot)$ near $p_0 = 0$ is exactly strong regularity at $x_0$.

Significance

Theorem 2.1 reduces the stability of a nonsmooth problem to a property of one linearised problem at the base point. Once strong regularity is checked at $x_0$, the solution exists, is locally unique and moves in a Lipschitz manner for every nearby parameter. Corollary 2.2 and Theorem 2.3 make this quantitative. Theorem 2.3 shows that a linear complementarity problem or a quadratic program approximates the nonlinear solution to first order. Theorem 2.4 is the analogue of Banach's perturbation lemma, which keeps an operator invertible under small perturbations. The later sections of the paper give checkable criteria for strong regularity: a Schur-complement test, a reduced-form test over polyhedral sets, and second-order conditions for nonlinear programs. Those criteria are the subject of the companion missions II–IV.

The theorems have been proved since 1980 and have been restated in textbooks. No machine-checked version of strong regularity or of this implicit-function theorem is known. Mathlib has the classical implicit- and inverse-function theorems for $C^1$ maps between Banach spaces, and the contraction mapping principle. It has nothing on normal-cone operators, generalized equations or Lipschitz localisations. The formalization adds this layer. It also shows that Theorem 2.1 needs no completeness of $X$.

Difficulty

The obvious approach is to apply the classical implicit-function theorem. It fails because $x \mapsto f(x) + \partial\psi_C(x)$ is set-valued and is not differentiable in any useful sense. The inverse is localised only to a neighbourhood $V$ and is single-valued only there. So every step must keep the iterates inside sets on which strong regularity says something. The neighbourhoods have to be chosen in the right order: $\delta$ from $\varepsilon$, then $U$ and $V$, then the ball radius $\rho$, then the parameter neighbourhood. The estimate (2.4) has to come out with the constant $\lambda + \varepsilon$ and no larger. The page applies the contraction principle in a space it calls only normed. A faithful proof must also obtain the fixed point without completeness of $X$, for example through the completeness of $X'$.

Formalization scope

• $X'$ is StrongDual ℝ X, the normal cone is a Set (StrongDual ℝ X) that is empty off $C$, and an inclusion $0 \in f(x) + \partial\psi_C(x)$ is written $-f(x) \in \partial\psi_C(x)$.
• Strong regularity is a predicate on $(C, f(x_0), f'(x_0), x_0, \lambda)$ with real $\lambda$. It requires existence, uniqueness in $V$ and the Lipschitz bound.
• $f$ is a total function $P \times X \to X'$ whose values off $P \times \Omega$ carry no hypothesis. The conclusion therefore asserts $W_\varepsilon \subseteq \Omega$.
• Differentiability is HasFDerivAt at every point of $\Omega$, for every $p$. Continuity of $f'$ at $(p_0, x_0)$ is joint and in operator norm.
• Uniqueness is uniqueness within $W_\varepsilon$, never global. Global uniqueness is false in general. Dropping uniqueness, or quantifying $\varepsilon$ after the neighbourhoods, would trivialize the goal, and the statements are written to exclude both.
• Theorem 2.1, Corollary 2.2 and Theorem 2.3 do not assume completeness, as printed. Theorem 2.4 assumes a Banach space, as printed.
• The contraction-principle milestone assumes completeness, under which the principle as invoked holds.
• Corollary 2.2 asks for its Lipschitz hypothesis on $N_\varepsilon \times V_\varepsilon$, sets that Theorem 2.1 produces. It is therefore stated on fixed neighbourhoods given in advance.
• Theorem 2.4 also asserts $\lambda\|A - A_0\| < 1$, which its proof secures.

A complete development needs the following:

• the mean-value inequality for Fréchet-differentiable maps on convex sets;
• the contraction principle on a closed ball;
• a fixed-point argument that obtains the fixed point through the complete space $X'$.

The definitions of normal cone and strong regularity are reusable for variational inequalities in general. Contributions are welcome at any level: proofs of the milestones, the goal from the milestones, or the companion results from the goal.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1):43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3