All missions

Motivation

A nonlinear program is rarely solved once. Its data are estimated, rounded, or varied on purpose in a parametric study, and an algorithm such as sequential quadratic programming replaces it at every iteration by a nearby linearised problem. Both uses need the same fact: near a solution, the Karush–Kuhn–Tucker (KKT) system should have exactly one solution for every small perturbation, and that solution should move Lipschitz-continuously with the perturbation. For problems with equality constraints only, or with strict complementary slackness, the classical implicit-function theorem gives this, as in Fiacco's sensitivity analysis (Fiacco 1976, reference [4] of the paper). Without strict complementarity the KKT system is not a smooth equation, and the classical theorem does not apply.

S. M. Robinson's paper Strongly regular generalized equations, Math. Oper. Res. 5 (1980) 43–62 introduced strong regularity to handle exactly this case. §2 of the paper proves an implicit-function theorem for generalized equations, §3 characterises strong regularity of linear generalized equations through a Schur complement, and §4, the subject of this mission, applies both to nonlinear programming. Its Theorem 4.1 identifies the conditions under which the KKT system is strongly regular. These conditions (strong second-order sufficiency and linearly independent binding gradients) became standard hypotheses in the stability theory of nonlinear programs and in the local convergence analysis of Newton-type methods.

Setting

Let $\Omega\subseteq\mathbb R^n$ be open and let $\theta:\Omega\to\mathbb R$, $g:\Omega\to\mathbb R^p$, $h:\Omega\to\mathbb R^q$ be Fréchet differentiable. The program is

$$\text{minimize } \theta(x)\quad\text{subject to}\quad g(x)\le0,\ h(x)=0.\qquad(4.1)$$

The Lagrangian is $\mathcal L(x,u,v)=\theta(x)+\langle u,g(x)\rangle+\langle v,h(x)\rangle$, and $\mathcal L'$ is its gradient in $x$.

For a set $C$ and a point $z$, the normal-cone operator $\partial\psi_C(z)$ is the set of vectors $y$ with $\langle y,c-z\rangle\le0$ for all $c\in C$ when $z\in C$, and the empty set when $z\notin C$. The KKT conditions of (4.1) are the generalized equation

$$0\in F(x,u,v)+\partial\psi_{\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q}(x,u,v),\qquad F(x,u,v)=\big(\mathcal L'(x,u,v),\,-g(x),\,-h(x)\big).\qquad(4.3)$$

Its middle block says $g(x)\le0$, $u\ge0$ and $\langle u,g(x)\rangle=0$.

A generalized equation $0\in F(z)+\partial\psi_C(z)$ is strongly regular at a solution $z_0$ (DEFINITION, p. 45) if its linearisation $T(z)=F(z_0)+F'(z_0)(z-z_0)+\partial\psi_C(z)$ satisfies the following. There are neighbourhoods $U$ of $0$ and $V$ of $z_0$ and a constant $\lambda$ such that, for every $y\in U$, the inclusion $y\in T(z)$ has exactly one solution $z=s(y)$ in $V$, and $s$ is $\lambda$-Lipschitz on $U$.

At a solution $(x_0,u_0,v_0)$ the inequality constraints split into three groups:

• $g^+$, with $g_i(x_0)=0$ and $u_{0,i}>0$;
• $g^0$, the weakly active ones, with $g_i(x_0)=0=u_{0,i}$;
• $g^-$, with $g_i(x_0)<0$.

Write $\mathcal L''=\mathcal L''(x_0,u_0,v_0)$ for the Hessian of the Lagrangian in $x$, $H=h'(x_0)$, $G^+=g^{+\prime}(x_0)$ and $G^0=g^{0\prime}(x_0)$. A square matrix is a P-matrix if all its principal minors are positive.

Formalization targets

Goal: Theorem 4.1 (p. 56)

Assume $\theta,g,h$ are twice differentiable at $x_0$ and $(x_0,u_0,v_0)$ solves (4.3). Assume also:

• (a′) strong second-order sufficiency: $\langle y,\mathcal L''y\rangle>0$ for all $y\ne0$ with $G^+y=0$ and $Hy=0$;
• (b) linear independence: the matrix $\begin{bmatrix}G^+\\G^0\\H\end{bmatrix}$ has full row rank.

Then

$$\text{(4.3) is strongly regular at }(x_0,u_0,v_0).$$

The Lipschitz constant is not fixed; the goal asserts that one exists.

Milestones

1. The matrix $K=\begin{bmatrix}\mathcal L''&H^T&G^{+T}\\-H&0&0\\-G^+&0&0\end{bmatrix}$ of (4.5) is nonsingular.
2. The equations (4.8) define $V,A,B$ uniquely, and the Schur complement $S=[G^0\ 0\ 0]\,K^{-1}\,[G^0\ 0\ 0]^T$ of (4.6) satisfies $S=G^0V=V^T\mathcal L''V$, so $S$ is symmetric.
3. A symmetric matrix is a P-matrix if and only if it is positive definite.
4. $S$ is positive definite.
5. The §4 criterion (p. 55): (4.3) is strongly regular at $(x_0,u_0,v_0)$ if and only if $K$ is nonsingular and $S$ is a P-matrix.

A further item formalizes the example (4.9)–(4.10) on pp. 56–57: a linear generalized equation in $\mathbb R^4$ whose unique solution satisfies the ordinary second-order sufficient condition and (b), yet is not strongly regular.

Significance

Strong regularity is the hypothesis of Robinson's implicit-function theorem (Theorem 2.1 of the paper). Theorem 4.1 therefore yields, for a parametrised nonlinear program, a locally unique and Lipschitz-continuous KKT point together with its multipliers, without strict complementary slackness. The same property underlies the local quadratic convergence of Josephy–Newton and SQP methods, and the criterion of milestone 5 is the form in which it is usually checked. The example of (4.10) shows that the ordinary second-order sufficient condition is not enough; the weakly active constraints have to be dropped from the cone on which $\mathcal L''$ must be positive.

All statements are proved in the paper. None of them, nor the notion of strong regularity, has a machine-checked proof on this platform. The matrix milestones (1–4) are self-contained linear algebra and can be proved independently. Milestone 3 for arbitrary symmetric matrices is a variant of Sylvester's criterion, which Mathlib does not currently state. Milestone 5 rests on §3 and the appendix of the paper (the Schur-complement criterion and the reduction of a linear generalized equation over a polyhedral set), which are the subjects of the companion missions II and III of this series.

Difficulty

The obvious argument would apply the classical implicit-function theorem to the active KKT equations. It fails because of the weakly active constraints. Near $(x_0,u_0,v_0)$ a constraint with $g_i(x_0)=0=u_{0,i}$ can become active or inactive under arbitrarily small perturbations, so the solution map is piecewise smooth, not smooth. Uniqueness has to hold across all the pieces simultaneously, which is a combinatorial condition: the P-matrix property of a Schur complement, not the nonsingularity of a single Jacobian. Example (4.10) shows that the natural guess (nonsingularity of every piece, guaranteed by ordinary second-order sufficiency) is insufficient: three distinct KKT points can coalesce at the origin.

The analytic part is also not routine. Strong regularity concerns the linearised problem with an arbitrary small perturbation on the right-hand side, including perturbations of the complementarity block. The criterion needs the reduction of §3 and the appendix, which localises the polyhedral set $\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q$ around the solution.

Formalization scope

• Spaces. Points of $\mathbb R^n$ are EuclideanSpace ℝ (Fin n). The triple $(x,u,v)$ lives in EuclideanSpace ℝ (Fin n ⊕ (Fin p ⊕ Fin q)), the Euclidean $\mathbb R^{n+p+q}$, so the normal cone uses the standard inner product. A product type, which carries the sup norm and no inner product, is deliberately not used.
• Normal cone. The operator includes the clause $z\in C$, so it is empty off $C$.
• Strong regularity. It is stated on the linearisation data, with a real Lipschitz constant $\lambda$, and requires existence, uniqueness in $V$ and the Lipschitz bound. Strong regularity at a point bundles a Fréchet derivative of $F$ there.
• Twice differentiable at $x_0$. This is encoded as $\theta$, $g_i$, $h_j$ differentiable on the open set $\Omega$ (the standing assumption of (4.1)), together with differentiability at $x_0$ of their gradients. It is not $C^2$ on $\Omega$, and symmetry of $\mathcal L''$ is not assumed; it follows.
• Matrix conventions. Positive definite means $\langle w,Mw\rangle>0$ for $w\ne0$, without symmetry. P-matrix quantifies over all nonempty principal index sets. The Schur complement is used only together with nonsingularity of (4.5), because Mathlib's inverse of a singular matrix is $0$.
• What must not be formalized. Replacing (a′) by the ordinary second-order sufficient condition, or restricting (b) to $G^+$ and $H$, gives a false or a different theorem. The milestones state exactly which constraints enter each condition: (a′) uses $G^+$ and $H$, and (b) uses $G^+$, $G^0$ and $H$. A formalization that drops the weakly active constraints from (b), or assumes strict complementarity, trivializes the goal to the classical implicit-function theorem.
• Infrastructure. A complete development needs the normal cone of a product of orthants, block-matrix inversion and Schur-complement identities, Sylvester-type criteria for symmetric matrices, and the reduction of a linear generalized equation over a polyhedral set to its reduced form. The linear-algebra milestones are reusable beyond this mission. Proofs of any milestone, and of the general P-matrix/positive-definite equivalence, are welcome.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1) (1980) 43–62. https://doi.org/10.1287/moor.5.1.43
• A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968 (reference [3] of the paper; second-order sufficient condition, Chapter 2).
• A. V. Fiacco, Sensitivity analysis for nonlinear programming using penalty methods, Mathematical Programming 10 (1976) 287–311 (reference [4] of the paper). https://doi.org/10.1007/BF01580379
• R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8 (1974) 189–211 (reference [1] of the paper). https://doi.org/10.1016/0024-3795(74)90055-4
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014 (modern account of strong regularity). https://doi.org/10.1007/978-1-4939-1037-3

Motivation

The Four-Colour Theorem was proved by Appel and Haken (1976–77) and re-proved by Robertson, Sanders, Seymour and Thomas (RSST, 1997) with a simpler, fully computer-checkable argument. Both proofs rest on reducibility: a configuration is reducible when every 4-colouring of the ring around it can be modified, by Kempe-chain recolouring, into one that extends inside. RSST make this precise with a purely combinatorial notion, the consistent set of edge-colourings of a circuit (§3 of their paper), which captures exactly which boundary colourings Kempe interchanges can reach from one another.

The oldest results about consistent sets predate the computer proofs. G. D. Birkhoff (1913) analysed rings of length 4 and 5 and showed that the possible "Kempe-closed" sets of boundary colourings on such short rings are very restricted. RSST restate Birkhoff's analysis in their language as (6.3) (rings of length 4) and (6.4) (rings of length 5). These two lemmas power the short-circuit subroutine of their quadratic 4-colouring algorithm (6.5), which colours a triangulation across a separating circuit of length 4 or 5.

Timeline:

• 1879–1890. Kempe introduces chain interchanges; Heawood finds the gap in Kempe's argument.
• 1913. Birkhoff, The reducibility of maps, studies rings of small size and introduces reducibility.
• 1976–77. Appel and Haken prove the Four-Colour Theorem.
• 1997. Robertson, Sanders, Seymour and Thomas give a new proof and an $O(n^2)$ colouring algorithm; consistent sets and lemmas (6.3), (6.4) appear in §§3 and 6.
• 2005–08. Gonthier formalizes the Four-Colour Theorem in Coq, with a different encoding of Kempe closure (chromograms on hypermaps).

Setting

Let $R$ be a circuit of length $k$: a cycle with edges $e_1, \dots, e_k$ in order, with no repeated vertices or edges. An edge-colouring of $R$ is a map $\kappa : E(R) \to \{-1, 0, 1\}$.

A match is an unordered pair $\{e, f\}$ of distinct edges, and a signed match is a pair $(\{e,f\}, \mu)$ with $\mu = \pm 1$. A signed matching is a set $M$ of signed matches such that for any two distinct members $(\{e,f\},\mu)$, $(\{e',f'\},\mu')$: the pairs $\{e,f\}$ and $\{e',f'\}$ are disjoint, and $e, f$ lie in the same component of $R$ with $e'$ and $f'$ deleted. Write $E(M)$ for the edges covered by $M$.

For $\theta \in \{-1,0,1\}$, the colouring $\kappa$ $\theta$-fits $M$ when $E(M)$ is exactly the set of edges with $\kappa(e) \neq \theta$, and for each $(\{e,f\},\mu) \in M$, $\kappa(e) = \kappa(f)$ holds if and only if $\mu = 1$. A set $\mathcal C$ of edge-colourings is consistent if for every $\kappa \in \mathcal C$ and every $\theta$ there is a signed matching $M$ that $\kappa$ $\theta$-fits such that $\mathcal C$ contains every edge-colouring that $\theta$-fits $M$.

Two edge-colourings are equivalent if one is obtained from the other by a permutation $\lambda$ of $\{-1,0,1\}$. On the circuit of length 5, $\mathcal A_{ij}$ ($i \neq j$) is the equivalence class of the colouring that is $1$ on $e_i$, $-1$ on $e_j$ and $0$ elsewhere. Then $\mathcal C_i = \mathcal A_{ij} \cup \mathcal A_{ik} \cup \mathcal A_{jk}$, where $e_j, e_k$ are the two edges sharing an end with $e_i$; $\mathcal D_i = \mathcal A_{ac} \cup \mathcal A_{ad} \cup \mathcal A_{bc} \cup \mathcal A_{bd}$, where $e_a, e_b, e_c, e_d$ are the other edges in order; and $\mathcal E = \mathcal A_{12} \cup \mathcal A_{23} \cup \mathcal A_{34} \cup \mathcal A_{45} \cup \mathcal A_{15}$. In Lean these are A, C5, D5, E5, and Consistent.

Formalization targets

Goal: Birkhoff's lemma for rings of length 5, (6.4)

$$\mathcal C \text{ consistent},\ \mathcal C \neq \emptyset,\ \mathcal C \cap \mathcal E \neq \emptyset \;\Longrightarrow\; \exists i,\ \mathcal C_i \subseteq \mathcal C \ \ \text{or}\ \ \exists i,\ \mathcal D_i \subseteq \mathcal C \ \ \text{or}\ \ \mathcal E \subseteq \mathcal C.$$

Milestones

1. Every consistent set is a union of equivalence classes (§6, p. 25): $\kappa \in \mathcal C \Rightarrow [\kappa] \subseteq \mathcal C$.
2. Claim (1) of the proof of (6.4): if $\mathcal A_{12} \subseteq \mathcal C$ then $\mathcal C$ includes one of $\mathcal A_{13}, \mathcal A_{15}$ and one of $\mathcal A_{23}, \mathcal A_{25}$.
3. Claim (2): if $\mathcal A_{13} \subseteq \mathcal C$ then $\mathcal C$ includes one of $\mathcal A_{23}, \mathcal A_{35}$.
4. The closure facts of §3, p. 8: $\emptyset$ is consistent, unions of two consistent sets are consistent, and every set $\mathcal S$ has a unique maximal consistent subset $\mathcal S'$.

Companion: Birkhoff's lemma for rings of length 4, (6.3)

With $\mathcal C_0, \dots, \mathcal C_3$ the classes of $(0,0,0,0)$, $(0,1,1,0)$, $(0,1,0,1)$, $(0,0,1,1)$, every non-empty consistent set includes one of $\mathcal C_0 \cup \mathcal C_1$, $\mathcal C_1 \cup \mathcal C_2$, $\mathcal C_2 \cup \mathcal C_3$, $\mathcal C_3 \cup \mathcal C_0$.

Significance

The result. (6.3) and (6.4) say that on rings of length at most 5 the Kempe-closed families of boundary colourings are rigid: a non-empty consistent family always contains one of a short explicit list of families. This is what makes separating circuits of length 4 and 5 harmless in a minimal counterexample and in the RSST colouring algorithm: whatever colourings one side of the circuit admits, the other side can be made to agree after Kempe changes.

Formalizing it. The Four-Colour Theorem itself is machine-checked (Gonthier, Coq), but that proof uses a different combinatorial encoding; RSST's notion of a consistent set, their signed matchings, and Birkhoff's ring lemmas in their formulation have no machine-checked version. The Four-Colour Theorem as such is not part of this mission; it is posed separately on the platform as the open goal FourColor.four_color. This mission builds the self-contained §3 layer (consistency) that RSST's reducibility computations rest on, proves two of its basic structural facts, and proves the two Birkhoff lemmas the paper uses. The definitions are reusable for a later formalization of (3.1) (lifts of tri-colourings form a consistent set) and of D-reducibility.

Difficulty

The statements are about finite objects: on a 5-ring there are $3^5 = 243$ edge-colourings, and the signed matchings have at most two matches. The difficulty lies elsewhere. Consistency quantifies over every member of $\mathcal C$, every $\theta$ and the existence of a signed matching together with a closure property, so a consistent set cannot be checked locally. The component condition on signed matchings is a statement about connectivity in a graph with two edges deleted, which must be connected to elementary arithmetic on the cycle before anything can be computed. An argument by brute force over all $2^{243}$ subsets is infeasible, so a proof has to pass through the structure of the classes $\mathcal A_{ij}$. The paper's own proof also uses the dihedral symmetry of the 5-ring without stating it as a lemma; it is not a milestone.

Formalization scope

• The circuit of length $k$ is SimpleGraph.cycleGraph k on Fin k; its edges are indexed by Fin k, edge $i$ being $\{i, i+1\}$ (mod $k$). The paper's $e_i$ is edge $i-1$: $\mathcal A_{12}$ is A 0 1, $\mathcal A_{15}$ is A 0 4, $\mathcal A_{25}$ is A 1 4, $\mathcal A_{35}$ is A 2 4.
• Colours are Mathlib's SignType; an edge-colouring is Fin k → SignType; $\mu \in$ ℤˣ; a match is a non-diagonal Sym2 (Fin k) of edge indices; a signed matching is a Set.
• The component condition is encoded literally with deleteEdges and Reachable, for both orders of every distinct pair; both halves of "consistent" are kept; equivalence uses Equiv.Perm SignType.
• C5 i uses edges $i \pm 1$; D5 i uses $(a,b,c,d) = (i+1, i+2, i+3, i+4)$ mod 5, the order along the path $R - e_i$, which is the reading the paper's proof requires ($\mathcal D_4 \supseteq \mathcal A_{25}, \mathcal A_{12}, \mathcal A_{13}, \mathcal A_{35}$).
• General-$k$ statements assume $k \ge 3$: circuits of length at most 2 have parallel edges and are not cycle graphs.
• Ruled out: dropping the component condition (crossing pairs would become signed matchings), a one-sided "consistent" (every set would be consistent and (6.4) false), any use of the junk class A i i, and degenerate circuits.

All definitions are in one file, FourColourRSST.Ring.Setting. Proofs of any item are welcome, as are lemmas making consistency decidable on small rings and the symmetry of the 5-ring under rotations and reflections.

Selected references

• N. Robertson, D. P. Sanders, P. Seymour, R. Thomas, The Four-Colour Theorem, J. Combin. Theory Ser. B 70 (1997), 2–44. https://doi.org/10.1006/jctb.1997.1750
• G. D. Birkhoff, The reducibility of maps, Amer. J. Math. 35 (1913), 115–128. https://doi.org/10.2307/2370276
• K. Appel, W. Haken, Every planar map is four colorable. Part I: Discharging, Illinois J. Math. 21 (1977), 429–490. https://doi.org/10.1215/ijm/1256049011
• G. Gonthier, Formal proof — the Four-Color Theorem, Notices Amer. Math. Soc. 55 (2008), 1382–1393. https://www.ams.org/notices/200811/tx081101382p.pdf

Motivation

Many problems of optimization and equilibrium reduce to a system of nonsmooth equations $F(x)=0$ with $F:\mathbb R^n\to\mathbb R^n$ locally Lipschitz but not differentiable: nonlinear complementarity problems written as $\min\{h(x),f(x)\}=0$, variational inequalities through the normal map, and Karush–Kuhn–Tucker systems of constrained programs. Newton's method in its classical form needs the Jacobian of $F$, which does not exist at the points of interest. Two kinds of generalized Newton methods replace it: one uses an element of a generalized Jacobian, the other uses the directional derivative $F'(x;d)$ and solves $F(x)+F'(x;d)=0$ for the step.

J.-S. Pang (Newton's method for B-differentiable equations, Math. Oper. Res. 15 (1990), doi:10.1287/moor.15.2.311) globalized the second kind with an Armijo line search on the merit function $g=\tfrac12\|F\|^2$, the damped Newton method, and proved that its accumulation points are zeros of $F$ under suitable conditions. Three questions were left open: does the whole sequence converge to one point, how fast, and when does the line search accept the full step? L. Qi (Convergence analysis of some algorithms for solving nonsmooth equations, Math. Oper. Res. 18 (1993) 227–244, doi:10.1287/moor.18.1.227) answered all three in his Theorem 4.3, under semismoothness and a regularity condition on the B-subdifferential. This mission formalizes that theorem and the results it rests on.

Timeline:

• 1977: Mifflin introduces semismooth functionals (doi:10.1137/0315061).
• 1987: Robinson introduces B-derivatives.
• 1990: Pang proposes the damped Newton method for B-differentiable equations and proves its global convergence (Theorem 4.2 in Qi's paper).
• 1993: Qi and Sun prove local superlinear convergence of the generalized-Jacobian Newton method at semismooth zeros (doi:10.1007/BF01581275); Qi's paper weakens the regularity condition to the B-subdifferential and proves Theorem 4.3.

Setting

Write $\mathbb R^n$ with the Euclidean norm, and let $F:\mathbb R^n\to\mathbb R^n$ be locally Lipschitz. The norm function is $g(x)=\tfrac12F(x)^{\mathsf T}F(x)=\tfrac12\|F(x)\|^2$.

The directional derivative of $F$ at $x$ in direction $h$ is the one-sided limit $F'(x;h)=\lim_{t\downarrow0}(F(x+th)-F(x))/t$. $F$ is B-differentiable at $x$ if $F'(x;h)$ exists for every $h$ and $F(x+h)=F(x)+F'(x;h)+o(\|h\|)$ (2.1).

Let $D_F$ be the set where $F$ is differentiable. The B-subdifferential $\partial_BF(x)$ is the set of all limits $\lim\nabla F(x_i)$ with $x_i\to x$, $x_i\in D_F$ (2.12). Its convex hull is Clarke's generalized Jacobian $\partial F(x)$. $F$ is strongly BD-regular at $x$ if every $V\in\partial_BF(x)$ is nonsingular. $F$ is semismooth at $x$ if $\lim Vh'$ over $V\in\partial F(x+th')$, $h'\to h$, $t\downarrow0$ exists for every $h$ (2.6). The directional derivative is semicontinuous of degree 2 at $x$ if $\|F'(x+h;h)-F'(x;h)\|\le L\|h\|^2$ for all $x+h$ in a neighbourhood of $x$ (2.5).

The damped Newton method (Algorithm 4.1) fixes $s>0$, $\beta\in(0,1)$, $\sigma\in(0,1/2)$. Given $x^k$ with $F(x^k)\neq0$, it takes a solution $d^k$ of the generalized Newton equation

$$F(x^k)+F'(x^k;d^k)=0, \tag{3.12}$$

lets $m_k$ be the first nonnegative integer $m$ with

$$g(x^k)-g(x^k+\beta^msd^k)\ \ge\ -\sigma\beta^ms\,g'(x^k;d^k), \tag{4.1}$$

and sets $\alpha_k=\beta^{m_k}s$, $x^{k+1}=x^k+\alpha_kd^k$.

Formalization targets

Goal: Theorem 4.3

Take $s=1$. Let $F$ be B-differentiable, let $\{x^k\}$ be a run of Algorithm 4.1 with $F(x^k)\neq0$ for all $k$, and let $x^*$ be an accumulation point of $\{x^k\}$ with $F(x^*)=0$, at which $F$ is semismooth and strongly BD-regular. Then

$$x^k\to x^*,\qquad \|x^{k+1}-x^*\|=o(\|x^k-x^*\|),\qquad \alpha_k=1\ \text{for all large }k.$$

The goal fixes no rate constant; it asserts convergence of the whole sequence, superlinearity and the eventual unit step.

Milestones

1. Corollary 3.4 (p. 236): for every $\varepsilon>0$ there is $\delta>0$ such that $\|x-x^*\|\le\delta$ and $F(x)+F'(x;d)=0$ imply $\|x+d-x^*\|\le\varepsilon\|x-x^*\|$ and $\|F(x+d)\|\le\varepsilon\|F(x)\|$.
2. Lemma 1 of Pang (proof of Theorem 4.3, p. 237): along a solution $d$ of (3.12), $g'(x;d)=-2g(x)$.
3. Unit step near $x^*$, (4.2)–(4.5) (p. 237): there is $\bar\delta>0$ such that $\|x^k-x^*\|\le\bar\delta$ implies $\alpha_k=1$, $x^{k+1}=x^k+d^k$ and $\|x^{k+1}-x^*\|\le\tfrac12\|x^k-x^*\|$.

Stronger statements

• Quadratic rate (Theorem 4.3, last sentence): if moreover $F'(\cdot,\cdot)$ is semicontinuous of degree 2 at $x^*$, then $\|x^{k+1}-x^*\|\le C\|x^k-x^*\|^2$ for all large $k$.
• Corollary 4.4 (p. 238): for an accumulation point $x^*$ at which $F$ is semismooth and strongly BD-regular, $F(x^*)=0$ iff $x^k\to x^*$ with eventually unit steps; and $F(x^*)\neq0$ iff $\{x^k\}$ diverges or $\alpha_k\to0$.

Significance

Theorem 4.3 is an attraction result: a regular zero that the damped iteration merely visits infinitely often captures the whole sequence, and from then on the method is the pure (undamped) directional Newton method with its fast local rate. Together with Pang's global theorem it gives a globally convergent method whose tail is superlinear, the standard template later followed by semismooth Newton methods for complementarity and variational inequality problems. Corollary 4.4 turns the theorem into a diagnostic: the behaviour of the step sizes decides whether a limit point solves the equation.

The theorems are proved in the paper. As far as a search of the platform shows, none of them, and no damped Newton method for B-differentiable equations, has a machine-checked proof. Formalizing them requires a reusable layer of nonsmooth analysis (directional derivatives of locally Lipschitz maps, the B-subdifferential and its local uniform invertibility) that other missions on semismooth Newton methods can import.

Difficulty

The local step of the obvious argument, "near $x^*$ the Newton step is accurate, so the Armijo test passes with $m=0$", needs two facts that are not automatic. First, the generalized Newton equation involves the nonlinear map $d\mapsto F'(x;d)$, not a matrix; the error estimate of Corollary 3.4 goes through a representation $F'(x;d)=Vd$ with $V\in\partial_BF(x)$, together with a uniform bound on $\|V^{-1}\|$ for $x$ near $x^*$. Second, the Armijo test involves $g'(x^k;d^k)$, whose value along a Newton direction has to be identified as $-2g(x^k)$. A further subtlety is global: an accumulation point only guarantees that the iterates come close to $x^*$ infinitely often, and the argument must show that once they are close enough they never leave, which needs the invariant ball of (4.5) and the fact that the step is exactly $d^k$ there.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (all norms are 2-norms, as in the paper), $n=0$ allowed. Every statement assumes $F$ locally Lipschitz (the paper's standing assumption of §1). The B-subdifferential, semismoothness and the directional derivative are the published definitions NonsmoothNewton.Shared.bJac, NonsmoothNewton.Local.SemismoothAt and NonsmoothNewton.Local.dirDeriv. Since dirDeriv takes a default value where the limit does not exist, (3.12) is encoded as the existence of the one-sided limit with value $-F(x^k)$. Nonsingularity is an explicit two-sided inverse. A run of Algorithm 4.1 records $d^k$, $\alpha_k$ and the minimality of $m_k$; without the minimality any $m$ would do and "$\alpha_k$ eventually becomes 1" would not be the paper's claim. An accumulation point is a cluster point of the sequence; superlinear convergence is $x^{k+1}-x^*=o(x^k-x^*)$.

Added hypotheses, disclosed in each item:

• Semismoothness on a neighbourhood of $x^*$ (Corollary 3.4 and everything built on it). The paper's proof uses $F'(x;d)=Vd$ with $V\in\partial_BF(x)$ at points $x$ near $x^*$ (its (2.16)), which its Lemma 2.6 proves only at semismooth points, while the printed hypothesis gives semismoothness at $x^*$ alone.
• $\varepsilon>0$ in Corollary 3.4, which prints $\varepsilon\ge0$; the case $\varepsilon=0$ is false in general.
• B-differentiability of $F$ everywhere, the setting of Pang's Theorem 4.2 that Theorem 4.3 refers to.

The theorems are not vacuous: runs of Algorithm 4.1 exist (for $F=\mathrm{id}$ the Armijo test passes at $m=0$), and a statement in which the line search index is not the first passing one, or in which $g'(x^k;d^k)$ is a default value, would not be the paper's theorem.

Contributions welcome: proofs of the milestones, in particular the representation $F'(x;d)=Vd$ and the local uniform invertibility of $\partial_BF$ (Lemma 2.6), which are reusable well beyond this mission.

Selected references

• L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Mathematics of Operations Research 18(1), 227–244, 1993. doi:10.1287/moor.18.1.227
• J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15(2), 311–341, 1990. doi:10.1287/moor.15.2.311
• L. Qi and J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58, 353–367, 1993. doi:10.1007/BF01581275
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15(6), 959–972, 1977. doi:10.1137/0315061
• S. M. Robinson, Local structure of feasible sets in nonlinear programming, Part III: Stability and sensitivity, Mathematical Programming Study 30, 45–66, 1987. (cited as [13] in Qi 1993)

Motivation

Many problems of operations research reduce to a system of nonsmooth equations $F(x)=0$ with $F:\mathbb R^n\to\mathbb R^n$ locally Lipschitz but not differentiable: the nonlinear complementarity problem $h(x)\ge 0$, $f(x)\ge0$, $h(x)^Tf(x)=0$ becomes $F(x)=\min\{h(x),f(x)\}=0$ componentwise, and variational inequalities, KKT systems and max-type equations admit similar reformulations. Newton's method is the natural local solver, but it needs a substitute for the Jacobian at points where $F$ is not differentiable.

Timeline:

• 1977. Mifflin introduces semismooth functionals.
• 1987–1990. Robinson proposes B-derivatives; Pang (1990) and Harker–Xiao (1990) study Newton methods based on directional derivatives (Math. Oper. Res. 15; Math. Programming 48).
• 1993. Qi and Sun (Math. Programming 58) prove local superlinear convergence of $x^{k+1}=x^k-V_k^{-1}F(x^k)$, $V_k\in\partial F(x^k)$, assuming every element of Clarke's generalized Jacobian $\partial F(x^*)$ is nonsingular.
• 1993. Qi (Math. Oper. Res. 18), the source of this mission, observes that this assumption already fails for $f(x)=|x|$, where $\partial f(0)=[-1,1]$ contains $0$, and restricts $V_k$ to the smaller B-subdifferential. Nonsingularity is then needed only on $\partial_B F(x^*)$.

Setting

A map $F:\mathbb R^n\to\mathbb R^m$ is locally Lipschitz throughout; the norm is the Euclidean 2-norm. Let $D_F$ be the set of points where $F$ is differentiable (almost every point, by Rademacher's theorem). The B-subdifferential of $F$ at $x$ is

$$\partial_B F(x)=\Big\{\lim_{i\to\infty}\nabla F(x_i)\;:\;x_i\to x,\ x_i\in D_F\Big\},$$

and Clarke's generalized Jacobian is its convex hull, $\partial F(x)=\operatorname{conv}\partial_B F(x)$. The directional derivative is $F'(x;h)=\lim_{t\downarrow0}(F(x+th)-F(x))/t$. $F$ is semismooth at $x$ if $\lim Vh'$ over $V\in\partial F(x+th')$, $h'\to h$, $t\downarrow 0$, exists for every $h$. A map $F:\mathbb R^n\to\mathbb R^n$ is strongly BD-regular at $x$ if every $V\in\partial_B F(x)$ is nonsingular.

The $\partial_B$ Newton method is

$$x^{k+1}=x^k-V_k^{-1}F(x^k),\qquad V_k\in\partial_B F(x^k), \tag{3.2}$$

with any choice of $V_k$, and the directional-derivative Newton method is $x^{k+1}=x^k+d^k$ with $F(x^k)+F'(x^k;d^k)=0$ (3.11)–(3.12). In Lean, $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\partial_B F$ is NonsmoothNewton.Shared.bJac F, $\partial F$ is clarkeJac F, semismoothness is NonsmoothNewton.Local.SemismoothAt, and a run of (3.2) is IsBDNewtonRun F x V.

Formalization targets

Goal: Theorem 3.1 (p. 234)

If $F(x^*)=0$ and $F$ is semismooth and strongly BD-regular at $x^*$, there is $\delta>0$ such that every $V\in\partial_B F(y)$, $\|y-x^*\|<\delta$, is nonsingular with $\|y-V^{-1}F(y)-x^*\|<\delta$, and every run of (3.2) from $\|x^0-x^*\|<\delta$ satisfies

$$x^k\to x^*,\qquad \|x^{k+1}-x^*\|=o(\|x^k-x^*\|),$$

and, when $F(x^k)\ne0$ for all $k$,

$$\lim_{k\to\infty}\frac{\|F(x^{k+1})\|}{\|F(x^k)\|}=0. \tag{1.9}$$

Milestones

1. Lemma 2.6 (p. 233): near a strongly BD-regular point, every $V\in\partial_B F(y)$ is nonsingular with $\|V^{-1}\|\le c$, and $\|h\|\le c\|F'(y;h)\|$ where $F$ is semismooth.
2. Lemma 2.2 (1) ⇔ (3) (p. 230): semismoothness at $x$ is equivalent to $Vh-F'(x;h)=o(\|h\|)$ for $V\in\partial F(x+h)$. This is the published item NonsmoothNewton.Local.theorem_2_3.
3. (2.2) (p. 229) at a semismooth point: $F(x+h)=F(x)+F'(x;h)+o(\|h\|)$. This is the published item NonsmoothNewton.Local.remark_2_17.
4. Corollary 3.2 (p. 235): for every $\varepsilon>0$, one $\partial_B$ Newton step near $x^*$ contracts $\|x-x^*\|$ and $\|F(x)\|$ by the factor $\varepsilon$.

Further statements of the paper in this mission

Lemma 2.3 (degree-2 semicontinuity, p. 230); the quadratic second paragraph of Theorem 3.1; Corollary 3.3 (the directional-derivative method, p. 235); Lemma 2.2 (1) ⇔ (2); and the counterexample of Final Remark (6) (pp. 243–244), which shows that (3.12) need not be solvable near a semismooth, strongly BD-regular zero.

Significance

Theorem 3.1 is the local convergence theorem for the semismooth Newton method in the form most used later: the B-subdifferential version under strong BD-regularity is what generalized Newton methods for complementarity problems (through the min and Fischer–Burmeister reformulations) rely on, because $\partial_B F$ is finite in typical piecewise-smooth examples while $\partial F$ is a polytope that may contain singular matrices. The statement (1.9) makes the method a descent method for $\|F\|$ near the solution, which is how the paper later globalizes it (damped Newton, §4; hybrid method, §6). Corollary 3.2 is reused verbatim in the analysis of the damped method.

The results are proved in the paper; none of them is formalized. The mission produces a machine-checked version of the local theory, on top of the published B-subdifferential and semismoothness definitions of the Qi–Sun series, and makes the Clarke-to-B-subdifferential refinement available to later missions.

Difficulty

The Clarke-Jacobian argument cannot be copied. There, nonsingularity of the compact convex set $\partial F(x^*)$ propagates to a neighbourhood by upper semicontinuity of $\partial F$. Here only the extreme set $\partial_B F(x^*)$ is assumed nonsingular, and its convex hull may contain singular matrices. Lemma 2.6 therefore has to work with limits of genuine Jacobians, and the error estimate (3.3) has to combine an estimate stated for $\partial F(x^k)$, namely Lemma 2.2, with the bound on $V_k^{-1}$, which exists only for $V_k\in\partial_B F(x^k)$. A second subtlety is (1.9), which needs a lower bound $\|x^k-x^*\|\le\frac{c}{1-\varepsilon}\|F(x^k)\|$ that does not follow from superlinear convergence alone.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with the 2-norm and the spectral operator norm, as the paper fixes ("we use 2-norms"). The dimension $n=0$ is allowed.

• Standing assumption. Every statement carries LocallyLipschitz F (§1, p. 227).

• Nonsingularity is the existence of a two-sided inverse $W$ (IsInverse V W), never a junk inverse. A run of (3.2) is written $V_k(x^{k+1}-x^k)=-F(x^k)$ without an inverse, so nonsingularity of $V_k$ is a conclusion.

• Quantifier order. $\delta$ is chosen before the run and serves every starting point within $\delta$ and every choice $V_k\in\partial_B F(x^k)$. Writing "for every run there is a $\delta$" would trivialize the theorem and is ruled out.

• (1.9) is stated under the paper's hypothesis $F(x^k)\ne0$ for all $k$, since otherwise the quotient is not defined.

• Disclosed deviations.

  • Corollary 3.2 is stated for $\varepsilon>0$ (the page prints $\varepsilon\ge0$, false at $0$).
  • Corollary 3.3 adds semismoothness of $F$ on a neighbourhood of $x^*$, which its printed proof uses through Lemma 2.6's (2.16).
  • $O(\cdot)$ and "quadratic" are pinned to explicit constants.

• Infrastructure needed.

  • Rademacher-type facts for $\partial_B F$: nonemptiness, compactness and closed graph. The platform already has WillR's proved lemmas NonsmoothNewton.Shared.exists_local_bJac_control, bJac_mem_of_tendsto, isCompact_bJac.
  • Perturbation bounds for inverses.
  • The relation between directional derivatives and $\partial_B F$ at semismooth points.

  These are reusable for the other two missions of this series and for later semismooth Newton developments. Proofs of the milestones, and alternative arguments, are welcome.

Selected references

• L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Math. Oper. Res. 18(1):227–244, 1993. https://doi.org/10.1287/moor.18.1.227
• L. Qi and J. Sun, A nonsmooth version of Newton's method, Math. Programming 58:353–367, 1993. https://doi.org/10.1007/BF01581275
• J.-S. Pang, Newton's method for B-differentiable equations, Math. Oper. Res. 15(2):311–341, 1990. https://doi.org/10.1287/moor.15.2.311
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15(6):959–972, 1977. https://doi.org/10.1137/0315061
• A. Shapiro, On concepts of directional differentiability, J. Optim. Theory Appl. 66:477–487, 1990. https://doi.org/10.1007/BF00940933

Why a one-sided market can have a core

Workers can form groups and produce an output that they divide through salaries. A group may object to a proposed allocation when it can pay all of its members at least as much and one member more. The central question is whether any allocation survives every such objection. Kelso and Crawford's 1982 paper gives a sufficient condition based on how an imaginary firm would demand workers as their salaries change. This is useful when production depends on combinations of workers, yet there is no actual employer side to the market.

The one-sided result belongs to a seven-mission series: 1, the salary-adjustment process; 2, continuous-salary core existence; 3, this one-sided theorem; 4, firm-optimality; 5, comparative statics; 6, returns to workers; and 7, the no-core example. Each mission can be read independently. None of Kelso and Crawford's results was on Prove2Me before this series. The paper itself notes that Theorem 3 is similar in spirit to Shapley's core-existence result but logically independent: Shapley's convex-game condition concerns second differences of a characteristic function, whereas this theorem uses a condition on input demand. Kelso and Crawford, footnote 3.

The market and its allocations

Let $W$ be a finite set of workers, with $m=|W|$. A coalition technology $v$ assigns a real output $v(C)$ to each worker set $C\subseteq W$. A one-sided allocation consists of a partition $P=(C_z)$ of all workers and one real salary $s_i$ for each worker. The parts of $P$ are disjoint and cover $W$. Each worker has a utility $\mu^i(s_i)$ that is continuous and strictly increasing in salary, so salary comparisons express the same preferences as utility comparisons.

The paper's individual rationality condition D1′ asks for nonnegative salaries and one aggregate resource constraint:

$$s_i\ge 0\quad(i\in W),\qquad \sum_{i\in W}s_i\le\sum_{C\in P}v(C).$$

It does not require each partition block to finance its own salaries. An improving coalition is a worker set $C$ with salaries $r_i\ge s_i$ for every $i\in C$, a strict inequality for at least one member, and $\sum_{i\in C}r_i\le v(C)$. A D1′ allocation is in the strict core D2′ when no improving coalition exists. The empty coalition cannot improve because it contains no member whose salary could rise. These are equations (12)–(15) on pages 1492–1493 of the source paper.

To state gross substitutes (GS), imagine $m+1$ identical firms, each with production $v$. At a salary vector $s:W\to\mathbb R$, a firm's profit from employing $C$ is $\pi(C;s)=v(C)-\sum_{i\in C}s_i$; a demanded set maximizes this profit over all worker subsets. GS says that if salaries rise coordinatewise from $s$ to $s'$, then for every demanded set at $s$ there is a demanded set at $s'$ containing all workers of the old set whose salaries stayed unchanged. The requirement is over all real salary vectors, as in the continuous market of Section 2.

Formalization targets

Goal: Theorem 3

Assume nonnegative marginal production (MP′), no free lunch (NFL), and GS for the identical fictitious firms:

$$v(C\cup\{i\})-v(C)\ge 0,\qquad v(\varnothing)=0,\qquad \operatorname{GS}(v).$$

The goal is the exact existence statement

$$\exists (P,s),\quad (P,s)\text{ is a one-sided strict-core allocation for }v.$$

Theorem 3 appears on page 1493 of Kelso and Crawford. Its two milestones are claims from the proof: every dummy firm has zero profit at a fictitious-market strict-core allocation, and that allocation induces a one-sided strict-core allocation. Mission 2 targets the paper's Theorem 2, which supplies existence of the fictitious-market allocation; this mission does not pose a duplicate specialized version of it.

What the result gives

The theorem ensures that workers can be partitioned and paid without any group being able to make at least one of its members strictly better off while preserving every member's prior salary. It turns a condition on a firm's reactions to wage increases into stability of a market containing no firms. The result also identifies a concrete boundary for the core-existence argument: the paper later constructs a market without GS that has no core allocation in its two-sided setting. Kelso and Crawford, Section 6.

The theorem is proved in the 1982 paper; this mission asks for machine-checked statements and proofs of its one-sided definitions, the two transfer claims, and Theorem 3. The local Lean files compile as open statements, and a concrete one-worker instance checks that MP′, NFL and GS can hold together. That local check is not a proof of Theorem 3. The definition of GS for a finite demand problem can be reused beyond this mission, but the dummy-firm construction and the one-sided D1′–D2′ predicates follow this paper's conventions.

Why the transfer is delicate

A strict-core allocation of a two-sided market controls coalitions containing a firm, while D2′ is expressed entirely through worker coalitions. The fictitious market has more firms than workers, which forces at least one firm to employ nobody. The proof must connect that observation to every firm's profit and then translate a one-sided improving coalition into a two-sided improvement. Individual rationality also has to preserve the paper's aggregate budget condition. Merely assigning each worker to a firm or showing nonnegative firm profits would leave these links unproved.

Formalization scope

Workers form an arbitrary finite type; the empty case is included. The fictitious firms have type Fin (m + 1), so their count is strictly greater than the worker count even when $m=0$. Salaries and output are real. In the fictitious market, every firm uses the same $v$, each worker's utility at every firm is $\mu^i(s)$, and reservation salary is zero, matching unemployment utility $\mu^i(0)$. The milestones retain arbitrary strictly increasing continuous functions $\mu^i$; Theorem 3 does not quantify over them because D1′ and D2′ compare salaries directly. Theorem 3's GS condition ranges over all real salary vectors, not a discrete salary grid.

Mathlib finite partitions contain nonempty parts. The paper permits empty indexed groups, but NFL makes them contribute zero output. The allocation model assigns every worker to one firm, and strict blocking allows any worker coalition, including the empty set, although strict improvement excludes that case. D1′ uses one total salary bound; a per-group bound would change the theorem. D2′ requires a strict gain in a worker's salary, not merely slack in the production budget. No vacuous regularity condition, fixed special technology, or restriction to a single worker is part of the mission goal.

Contributions are welcome on the finite partition interface, properties of profit-maximizing demand under GS, the zero-profit claim, and the transfer from fictitious firms to worker coalitions. The shared market and demand definitions are kept in their own module so they can be consolidated with the other missions of this paper.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, pp. 1483–1504. DOI: 10.2307/1913392.
• L. S. Shapley, Cores of convex games, International Journal of Game Theory 1, 1971, pp. 11–26. DOI: 10.1007/BF01753431.

Motivation

Labor markets match heterogeneous workers to heterogeneous firms, and the terms of each match — the salary — are negotiated. Kelso and Crawford (Econometrica 50 (1982)) studied such a market in which a firm may hire many workers, its output depends on the whole set it hires, and salaries are set worker by worker. Their model contains the marriage problem of Gale and Shapley (1962) and the assignment game of Shapley and Shubik (1971) as special cases, and its gross substitutes condition later became the central hypothesis of the theory of matching with contracts and of ascending auctions for indivisible goods (Hatfield and Milgrom, AER 2005; Gul and Stacchetti, JET 1999).

Markets of this kind usually have many stable outcomes, so which one arises depends on how the market is organized. Gale and Shapley showed that their deferred-acceptance procedure picks the stable matching that is best for the proposing side. Crawford and Knoer (Econometrica 1981) proved the analogue for one-to-one matching with money. Theorem 4 of Kelso and Crawford extends it to firms that hire many workers, under gross substitutes: the paper's salary-adjustment process, in which firms make offers, ends at the end of the strict core that favors the firms.

Setting

There are finitely many workers $i \in W$ and firms $j \in F$. Worker $i$ values working for firm $j$ at salary $s$ by $u^i(j; s)$, strictly increasing and continuous in $s$. Firm $j$ produces $y^j(C)$ when it hires the set $C$ of workers and earns the profit $\pi^j(C; s^j) = y^j(C) - \sum_{i\in C} s_{ij}$ at the salary vector $s^j$. The number $\sigma_{ij}$ is the starting permitted salary for $i$ at $j$; Section 2 initially defines it as a reservation salary, and Section 5 permits it to be perturbed. The paper's standing assumptions are (MP), $y^j(C\cup\{i\}) - y^j(C) - \sigma_{ij} \ge 0$ for $i \notin C$; (NFL), $y^j(\varnothing) = 0$; and (GS): if $C$ maximizes firm $j$'s profit at $s^j$ and salaries rise weakly to $\tilde s^j$, some profit-maximizing set at $\tilde s^j$ still contains every worker of $C$ whose salary did not change.

In a discrete market with unit $\delta > 0$, firm $j$ may offer worker $i$ only the salaries $\sigma_{ij} + k\delta$, $k \in \mathbb{N}$. An allocation assigns every worker $i$ to a firm $f(i)$ at a salary; $C^j$ is the set hired by $j$. It is individually rational if every worker gets at least $\sigma_{if(i)}$ and every firm a nonnegative profit. A firm and a set of workers at permitted salaries improve upon it if all of them are weakly better off and one of them strictly; they strictly improve upon it if all are strictly better off. Discrete strict core allocations (D2) admit no improving coalition, discrete core allocations (D3) no strictly improving one.

The salary-adjustment process (R1–R5) starts with permitted salaries $s_{ij}(0) = \sigma_{ij}$ and offers from every firm to every worker. In each round, each firm offers jobs to a profit-maximizing set at its current permitted salaries, repeating unrejected offers; each worker holds a favorite offer and rejects the others; a rejected firm's permitted salary for that worker rises by $\delta$. The process stops in a round with no rejections. A worker is (strictly) $s$-possible for firm $j$ if some discrete (strict) core allocation assigns him or her to $j$ at salary $s$. The no-ties conditions are (NTW): a worker who is $s_{ij}$-possible for $j$ is never indifferent between $(j, s_{ij})$ and any permitted salary at another firm; and (NTF): a firm is never indifferent between its profit in a discrete core allocation and the profit from another nonempty set of workers at permitted salaries.

Formalization targets

Goal: Theorem 4 (p. 1495)

Under regularity, (MP), (NFL), (GS) on the permitted salary vectors, (NTW) and (NTF): every run of the process stops at some round, and at every stopping round $T$ the resulting allocation $\phi$ is a discrete strict core allocation with

$$\pi^j(C^j_{A'}; s'^j) \le \pi^j(C^j_\phi; s^j(T)) \qquad \text{for every firm } j \text{ and every discrete strict core allocation } A'.$$

Milestones (proof of Theorem 4, p. 1495)

1. Every equilibrium of the process is a discrete strict core allocation.
2. No worker ever rejects a firm at a salary $s$ at which he or she is strictly $s$-possible for it.
3. For every strict core allocation $(f; s')$, every round $t$ and every worker $i$: $s_{if(i)}(t) \le s'_{if(i)}$.

Significance

Theorem 4 says that the outcome of a decentralized ascending process, in which firms make the offers, is not an arbitrary stable outcome but the one best for every firm simultaneously. This existence of a firm-optimal point of the strict core is itself a consequence. Its Corollary (uniqueness of the equilibrium, mission 5 of this series) and Theorem 5 (an entering firm helps every worker, a departing worker hurts every firm, also mission 5) are both proved from it.

The result has been proved on paper since 1982, and nothing of this paper was on Prove2Me before this series. The mission produces a machine-checked version of the paper's model, of the salary-adjustment process for every tie-breaking rule, and of the firm-optimality argument. The no-money analogue, Gale and Shapley's optimality theorem for college admissions, has a proved formalization on the platform (GS62CollegeAdmissions.PaperInterface.theorem2_applicant_optimality); it does not involve salaries and is credited, not reused.

The series has seven missions: 1 (Theorem 1, convergence to a discrete core allocation), 2 (Theorem 2, the continuous strict core), 3 (Theorem 3, one-sided markets), 4 (this mission), 5 (comparative statics, Theorem 5), 6 (Theorem 6, gross substitutes and returns to workers), 7 (the no-core example of Section 6). This mission does not depend on the others: it states its own copy of the model.

Difficulty

The process is defined for every tie-breaking rule of firms and workers, so the claim concerns an entire family of executions, each indexed by rounds and carrying offers, tentative acceptances and salaries. The firm-optimality statement compares the process outcome with every strict core allocation, objects defined by a nonexistence condition over all coalitions and permitted salaries. The step that does not follow from Theorem 1 alone is that rejections never occur at a strictly possible salary. That claim is about the entire history of a run, not about its final round, and it ties a property of the core to every intermediate rejection. Without the no-ties hypotheses the paper guarantees only that the process stops at a discrete core allocation (D3, Theorem 1).

Formalization scope

Workers and firms are arbitrary finite types, with at least one firm; salaries are real numbers; larger utility is better. A discrete market is given by the unit $\delta > 0$, and the permitted salaries are $\sigma_{ij} + \delta\mathbb{N}$ (the paper's unit is 1; Theorem 2 lets it shrink, so it is kept general). The starting salaries $\sigma_{ij}$ are data; the relation $u^i(j;\sigma_{ij}) = u^i(0;0)$ is not assumed, because Section 5 perturbs $\sigma_{ij}$ independently of $u^i(0;0)$ to obtain (NTW), and under that relation (NTW) typically fails in round 0. Allocations assign every worker to a firm. (GS) is imposed on the permitted salary vectors of the discrete market only.

Explicit readings of the paper's phrases:

• "converges to" means: every run stops at some round, and every stopping round yields the stated allocation;
• "any other strict core allocation" means any discrete strict core allocation of the same discrete market;
• "at least as good for every firm" is a weak profit inequality at every firm;
• (NTW) and (NTF) are about discrete core allocations (D3), as printed, and "any other non-empty set of workers" in (NTF) is read as a nonempty set different from $C^j$;
• a run of R1–R5 is any sequence of salaries, offers and tentative acceptances obeying the rules, with all ties broken arbitrarily; the statements cover every run.

Statements that quantify over runs would be empty if no run existed, and (NTW), (NTF) are hypotheses about the core that could in principle be contradictory; a sorry-free local check confirms all hypotheses on a market with one firm and one worker and exhibits a run that stops at a strict core allocation, so the goal is not vacuous. Trivializing readings — comparing with continuous strict core allocations, imposing (NTW)/(NTF) only on strict core allocations, or comparing a single firm — are excluded by the statement.

Infrastructure needed: the model, the run encoding, and lemmas about runs (salaries are monotone and stay on the grid, every worker always holds an offer, every run stops — Theorem 1). These are reusable for missions 1 and 5. Contributions to any milestone, and alternative proofs, are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1912758
• D. Gale and L. S. Shapley, College admissions and the stability of marriage, American Mathematical Monthly 69(1), 1962, 9–15. https://doi.org/10.2307/2312726
• L. S. Shapley and M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466
• F. Gul and E. Stacchetti, Walrasian equilibrium with gross substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531

Motivation

Branch and bound was introduced for integer programming by Land and Doig (1960) and for the travelling salesman problem by Little, Murty, Sweeney and Karel (1963). Ignall and Schrage (1965) were among the first to apply it to machine scheduling. They give lower bounds for two permutation flow-shop problems: the makespan on three machines, and the mean completion time on two. Their Appendix then asks how the method depends on the units and the origin of the data. Its THEOREM says that changing the location and the scale of all processing times changes neither the optimal sequence nor the path the branch-and-bound procedure takes.

The statement matters for computational experiments of the kind the paper reports. Run times and node counts measured on one jobset carry over to every jobset obtained from it by a positive affine change of the processing times, so a test family need only vary the shape of the data, not its location and scale. It is also a correctness property of the procedure: a branch-and-bound method whose behaviour depended on the time unit would be suspect.

Setting

There are $n$ jobs, and every job visits the machines in the same order: $A$, then $B$ (two-machine problem), or $A$, $B$, then $C$ (three-machine problem). Job $i$ has nonnegative processing times $a_i, b_i$ (and $c_i$). Following Johnson (1954), both problems are restricted to permutation schedules. A full sequence $\sigma$ lists the jobs in the order in which every machine processes them, and each operation starts as early as possible. The makespan of $\sigma$ is the time machine $C$ finishes its last job. The completion time $d_i$ of job $i$ is the time machine $B$ finishes it, and the two-machine objective is $\sum_i d_i$, which is $n$ times the mean completion time.

A node $J_r$ is a partial sequence of $r$ distinct jobs, and $\bar J_r$ is the set of the $n-r$ jobs it has not scheduled. For three machines, $\mathrm{TIMEA}, \mathrm{TIMEB}, \mathrm{TIMEC}(J_r)$ are the times the machines finish $J_r$, and the lower bound (p. 401) is

$$LB(J_r)=\max\Big[\mathrm{TIMEA}+\sum_{\bar J_r}a_i+\min_{\bar J_r}(b_i+c_i),\ \mathrm{TIMEB}+\sum_{\bar J_r}b_i+\min_{\bar J_r}c_i,\ \mathrm{TIMEC}+\sum_{\bar J_r}c_i\Big].$$

For two machines, $\hat T_r$ and $\hat S_r$ are the minima over orderings of $\bar J_r$ of two explicit sums $T_r$, $S_r$ (pp. 405–406), and the lower bound is $LB(J_r)=\sum_{i\in J_r}d_i+\max(\hat T_r,\hat S_r)$.

The branch-and-bound procedure (p. 402) keeps a list of nodes ranked by $LB$, starting from the root alone. At each step it removes the first node and inserts each of its children $J_r\,j$ ranked into the list. On ties a new node goes before an old one (p. 403). It stops when the first node has scheduled $n-1$ jobs, which fixes the whole sequence. The list after $k$ steps is $\mathrm{run}_{LB}(k)$.

Problems $P'$ (data $a'_i,b'_i,c'_i$) and $\tilde P$ are related by a change of location and scale when

$$\tilde a_i = H(a'_i+G),\qquad \tilde b_i=H(b'_i+G),\qquad \tilde c_i = H(c'_i+G),\qquad H,G>0.$$

Formalization targets

Goal: the Appendix THEOREM (p. 411)

For both the three-machine makespan problem and the two-machine sum-of-completion-times problem:

$$\sigma \text{ is optimal for } \tilde P \iff \sigma \text{ is optimal for } P', \qquad \mathrm{run}_{LB_{\tilde P}}(k)=\mathrm{run}_{LB_{P'}}(k)\ \text{ for all } k .$$

Milestones, in the order of the paper's proof

1. Adding $G$ to every processing time raises the completion time of the $r$-th job on machine $M$ by $G(r+M-1)$.
2. On two machines, $\sum_i d_i$ rises by $\tfrac12 Gn(n+3)$ for every sequence.
3. On two machines, $\hat T_r$ and $\hat S_r$ rise by $G[r(n-r)+\tfrac12(n-r)(n-r+1)+(n-r)]$, $\sum_{J_r}d_i$ by $\tfrac12Gr(r+3)$, and $LB(J_r)$ by $\tfrac12Gn(n+3)$, for $1\le r\le n-1$.
4. On three machines, every makespan and every $LB(J_r)$ with $1\le r\le n-1$ rises by $G(n+2)$.
5. Multiplying all processing times by $H>0$ multiplies all these quantities by $H$.
6. If $LB'=\varphi\circ LB$ on the nodes with $1\le r\le n-1$, for a strictly increasing $\varphi$, the two runs coincide at every step.

Significance

The THEOREM makes the method's behaviour a function of the shape of the data alone, not of its location or scale. This justifies normalizing test data, comparing running times across jobsets that differ by a change of units, and reporting results for one representative of each class. The proof also isolates a general principle: a deterministic best-first search depends on its bound only through the order the bound induces on the nodes it compares. Milestone 6 states that principle for the procedure of p. 402 with an arbitrary bound, so it applies to any other bound plugged into the same procedure.

As far as is known, no machine-checked version of this result or of the two lower bounds exists. The formalization needs the paper's procedure, with its tie rule, as an explicit deterministic function, and both lower bounds as functions of a node. The mission produces both, along with exact shift identities for every quantity the procedure uses.

Difficulty

The obvious argument is "adding $G$ adds a constant to everything", and it is not literally true. The constant depends on the position of a job and on the machine, so the identities must be computed term by term: maxima over machine-availability times commute with the shift only because both arguments move by the same amount, and that fails at the first job if processing times may be negative. The paper's own accounting contains a slip, the missing factor $G$ in $\tfrac12 r(r+3)$. Its claim that "all lower bounds" of the three-machine problem rise by $G(n+2)$ is false at the root, where $\mathrm{TIMEB}=0$ does not move. The run equality therefore has to use the fact that the root is never compared with another node. The minima $\hat T_r$, $\hat S_r$ range over all orderings of $\bar J_r$, so their shift requires every ordering to move by the same amount. Finally, "the same path" has to be shown for the procedure's insertion with ties, step by step.

Formalization scope

• Jobs are Fin n, numbered from $0$. Processing times are real, and the shift statements and the goal assume them nonnegative, the paper's standing convention for durations. With negative times the goal is false (a three-job counterexample is recorded in the goal's statement). Scaling needs no sign condition.
• The schedules of full sequences are Johnson's published as-soon-as-possible schedules (JohnsonFlowShop.ThreeStage.asapDone, JohnsonFlowShop.TwoStage.asapC2). Node attributes are computed by the same recursion on lists.
• The two-machine objective is $\sum_i d_i$ instead of the mean; the two have the same minimizers.
• $\hat T_r$ and $\hat S_r$ are minima over all orderings of $\bar J_r$, not values at a sorted order.
• Terminal nodes have depth $n-1$. The procedure inserts children one at a time in increasing job index, each before every node of equal bound. Dominance discarding is not part of it.
• Explicit readings. "The same sequence is optimal for both problems" means the sets of optimal sequences are equal, stated as an iff for every $\sigma$. "Will follow the same path" means $\mathrm{run}(k)$ is equal for both problems at every $k$. The paper's "all lower bounds" in the three-machine shift is restricted to nodes with $1\le r\le n-1$. The hypotheses $H>0$ and $G>0$ are kept as stated.
• Trivializations ruled out. A goal asserting only that some common optimal sequence exists, or only that the optimal values are related, would be weaker than the THEOREM. The goal states the iff and the equality of runs, with the procedure fixed independently of the data except through the bound.
• The procedure, the node attributes and the lower bounds are also drafted in missions 1 and 2 of this series. Milestone 6 is reusable for any bound used with the same procedure. Proofs of any milestone are welcome. Generalizations, such as arbitrary real $G$ in the shift identities, are welcome as separate items.

Credit: Johnson (1954) for the reduction to permutation schedules and the published schedule definitions. No platform item treats flow-shop lower bounds or branch and bound over sequences. The nearest is the branch-and-bound mission BiconvexProg.BranchBound (Al-Khayyal and Falk), an unrelated algorithm for biconvex programs.

Selected references

• E. Ignall, L. Schrage, Application of the branch and bound technique to some flow-shop scheduling problems, Operations Research 13(3), 400–412, 1965. https://doi.org/10.1287/opre.13.3.400
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• A. H. Land, A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129
• J. D. C. Little, K. G. Murty, D. W. Sweeney, C. Karel, An algorithm for the traveling salesman problem, Operations Research 11(6), 972–989, 1963. https://doi.org/10.1287/opre.11.6.972