All missions

Motivation

The subgradient method for a convex function $f$ moves from $x_k$ against a subgradient $g_f(x_k)$, and everything hinges on the step length. Divergent-series stepsizes guarantee convergence but are slow and need no information about $f$. When the optimal value $f^*$, or any level $c$ that is known to be attainable, is available, B. T. Polyak proposed in 1969 the step

$$x_{k+1} = x_k - \frac{\gamma\,[f(x_k) - c]}{\|g_f(x_k)\|^2}\, g_f(x_k),$$

which uses the current gap $f(x_k) - c$ to scale the move. This Polyak stepsize is still the reference adaptive rule in nonsmooth convex optimization, in the solution of convex feasibility problems, and in the Lagrangian relaxation heuristics of integer programming (Held–Wolfe–Crowder, Camerini–Fratta–Maffioli), where it is known under the name "relaxation step".

Section 2.4 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) places Polyak's rule in the framework of Fejér-type approximations developed by I. I. Eremin: an iteration whose map strictly decreases the distance to every point of a target set. It then proves convergence of the rule, linear rates under growth conditions, its behaviour when the level is set too low, and a property of the conjugate-subgradient direction of Camerini, Fratta and Maffioli (1975).

Timeline:

• 1965–1969: Eremin introduces Fejér mappings for systems of convex inequalities.
• 1969: Polyak, Minimization of unsmooth functionals, proposes the step with the known optimal value and proves convergence and a linear rate under a sharp-minimum condition.
• 1975: Camerini, Fratta and Maffioli combine the Polyak step with a conjugate direction for Lagrangian relaxation.
• 1985: Shor's book collects these results in Section 2.4 (Theorems 2.10–2.16).

Setting

$E_n$ is the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$. A subgradient selection is a map $g_f$ with $g_f(x)$ a subgradient at every $x$; nothing else is assumed about it, in particular not continuity.

For a nonempty set $M \subseteq E_n$, a map $\varphi : E_n \to E_n$ is $M$-Fejér if $\varphi(y) = y$ and $\|\varphi(x) - y\| < \|x - y\|$ for all $y \in M$ and $x \notin M$.

For a convex $f$ with $f^* = \inf f$ and a level $c \ge f^*$, let $M(c) = \{x : f(x) \le c\}$. Polyak's method (2.32) is the iteration $x_{k+1} = \varphi_c(x_k)$ with the map displayed above for $x \notin M(c)$ and $\varphi_c(y) = y$ on $M(c)$; the factor $\gamma$ is fixed in $(0, 2)$.

The conjugate-subgradient procedure (2.38), for a convex $f$ with minimum point $x^*$ and $f^* = f(x^*)$, is

$$x_{k+1} = x_k - h_k s_k, \quad h_k = \frac{[f(x_k) - f^*]\gamma_k}{\|s_k\|^2}, \qquad s_0 = g_f(x_0),\quad s_k = g_f(x_k) + \beta_k s_{k-1}.$$

Formalization targets

Goal: Theorem 2.11

If $0 < \gamma < 2$ and $M(c) \neq \emptyset$, then for any $x_0 \in E_n$

$$\exists k^* : x_{k^*} \in M(c) \qquad \text{or} \qquad \lim_{k \to \infty} x_k \text{ exists and lies in } M(c).$$

The goal fixes no constant and no rate; it asserts only that the method finds a point of the level set, in finite time or in the limit.

Milestones

1. Theorem 2.10. Iterates of a continuous $M$-Fejér map converge to a point of $M$.
2. Inequality (2.33). For $x_k \notin M(c)$ and $y \in M(c)$,

$$\|x_{k+1} - y\|^2 \le \|x_k - y\|^2 - \gamma(2-\gamma)\frac{[f(x_k) - c]^2}{\|g_f(x_k)\|^2} < \|x_k - y\|^2 .$$

3. Theorem 2.12. Under $f(x) - f^* \ge m\|x - x^*\|^2$ and an $L$-Lipschitz gradient near $x^*$, with $c = f^*$: $\|x_k - x^*\| \le q^k \|x_0 - x^*\|$, $q = (1 - \gamma(2-\gamma)m^2/L^2)^{1/2} < 1$.
4. Theorem 2.13. Under the sharp-minimum condition $f(x) - f(x^*) \ge m\|x - x^*\|$ and subgradients bounded by $L$ near $x^*$, with $c = f(x^*)$: $\|x_{k+1} - x^*\| \le q\|x_k - x^*\|$.
5. Theorem 2.14. If $\min \psi = d > 0$ and the method runs with $c = 0$, then $\lim_k \min_{0 \le i \le k} \psi(x_i) \le 2d/(2-\gamma)$.
6. Theorem 2.15. For (2.38) with $0 < \gamma_k \le 1$, $\beta_k \ge 0$: $(x_k - x^*, s_k) \ge (x_k - x^*, g_f(x_k))$.
7. Theorem 2.16. With the Camerini–Fratta–Maffioli coefficient $\beta_k$ and $0 \le \alpha_k \le 2$: $(x_k - x^*, s_k)/\|s_k\| \ge (x_k - x^*, g_f(x_k))/\|g_f(x_k)\|$.

Significance

Theorem 2.11 is the convergence guarantee of the most widely used adaptive step rule for nonsmooth convex problems. With $c = f^*$ it yields a minimizer; with $c > f^*$ it solves the convex inequality $f(x) \le c$, and applied to $\psi = \max_i f_i^+$ it solves consistent systems of convex inequalities. The linear rates of Theorems 2.12–2.13 are the prototype of the "sharpness implies linear convergence" results of modern first-order methods, and Theorem 2.14 quantifies the loss when the level is underestimated, which is the situation of every practical variant that estimates $f^*$ on the fly. Theorems 2.15–2.16 are the justification of the conjugate-subgradient directions used in Lagrangian relaxation.

All results are classical and proved on paper. None of them is formalized on Prove2Me: the platform has a smooth, strongly convex Polyak gradient-descent bound (a different theorem) and Fejér-monotonicity statements for polyhedral relaxation methods, but no Polyak subgradient step, no $M$-Fejér map and no conjugate-subgradient procedure. The mission produces machine-checked versions of the whole section, with the page's misprints corrected where the proof and the statement disagree.

Difficulty

The obvious argument for the goal is to observe that $\varphi_c$ is $M(c)$-Fejér, by (2.33), and invoke Theorem 2.10. That argument fails: Theorem 2.10 needs a continuous map, and $\varphi_c$ depends on an arbitrary subgradient selection, which is discontinuous wherever $f$ is not differentiable. The book says so explicitly. Fejér monotonicity gives boundedness and a limit of each distance $\|x_k - y\|$, but convergence of the whole sequence to a single point of $M(c)$, and the fact that an accumulation point cannot lie outside $M(c)$, have to be obtained without continuity of the map.

For Theorem 2.14 the level $c = 0$ lies strictly below the minimum, so $M(0) = \emptyset$, the target set of the iteration as run is empty, no Fejér property is available for it, and the theorem controls only the best value found, not the iterates.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued on all of $E_n$ and ConvexOn ℝ Set.univ f.
• The subgradient selection is universally quantified; no theorem assumes continuity of it.
• Iterations are sequences x : ℕ → E_n with the recursion as a hypothesis; the first term is arbitrary.
• Polyak's step map is defined piecewise: it returns $x$ on $M(c)$ (as the book sets $\varphi_c(y) = y$) and at $g_f(x) = 0$. No statement relies on Lean's convention $x/0 = 0$. The same holds for $h_k$ when $s_k = 0$.
• $M(c) \neq \emptyset$ is a hypothesis of the goal: the book's proof picks $y \in M(c)$, and for $c = f^*$ not attained the conclusion is false (for $f = e^x$, $c = 0$, the method moves by $\gamma$ each step and diverges).
• "$\lim x_k \in M(c)$" is the existence of a limit in $M(c)$, not a statement about cluster points.
• $\gamma \in (0, 2)$ is stated in every theorem on Polyak's method; the book fixes this range at Theorem 2.11.
• Theorem 2.12's "strongly convex" is used through its displayed growth condition only; the statement is made for convex $f$ satisfying it, with $L > 0$ and $q$ computed with Real.sqrt.
• Theorem 2.13 assumes the bound $\|g\| \le L$ on subgradients in the ball, which is what the proof uses; a Lipschitz constant on the closed ball alone does not give it, and the printed statement fails without it.
• Theorem 2.14 is stated with "$\le 2d/(2-\gamma)$"; the printed "$=$" is false in general.
• Theorem 2.16's inequality is stated at indices where $s_k \neq 0$ and $g_f(x_k) \neq 0$.

A formalization in which $M(c)$ may be empty, the selection is assumed continuous, or the step divides by zero through Lean's conventions would be a different theorem; these are ruled out above.

Needed infrastructure: Fejér monotone sequences in finite dimensions (bounded, with convergent distances), the subgradient inequality, and the fact that a zero subgradient characterizes a minimum. These are reusable for every subgradient-type method. Contributions of general lemmas on Fejér-monotone sequences are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §2.4, pp. 36–42. https://doi.org/10.1007/978-3-642-82118-9
• B. T. Polyak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9(3), 1969, 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
• I. I. Eremin, The relaxation method of solving systems of inequalities with convex functions on the left-hand side, Soviet Mathematics Doklady 6, 1965, 219–222.
• P. M. Camerini, L. Fratta, F. Maffioli, On improving relaxation methods by modified gradient techniques, Mathematical Programming Study 3, 1975, 26–34.

Motivation

The simplex method is the standard algorithm for linear programming, and its correctness rests on one question: does it stop? Each pivot of the method moves from one dictionary to another without decreasing the objective value, but a pivot can leave the objective unchanged. When that happens repeatedly, the method can return to a dictionary it has already visited and loop forever. This behaviour, cycling, is not hypothetical: Vanderbei's Chapter 3 exhibits a problem with four decision variables and three constraints on which the "largest coefficient" entering rule with a natural tie-breaking rule cycles through six dictionaries (Vanderbei 2014, pp. 26–27).

The chapter answers the question with two pivoting rules under which the simplex method provably terminates, and then draws the consequence that makes linear programming a finite theory: the fundamental theorem of linear programming. This mission formalizes the chapter's four numbered theorems in Vanderbei's own setting of standard-form problems with slack variables.

Timeline. Hoffman (1953) and Beale (1955) gave the first examples of cycling. The perturbation and lexicographic methods go back to Charnes (1952) and to Dantzig, Orden and Wolfe (1955). Bland (1977) introduced the smallest-index rule and proved that the simplex method terminates under it (Bland 1977).

Setting

A linear program in standard form has $m$ constraints and $n$ decision variables:

$$\text{maximize } \sum_{j=1}^n c_j x_j \quad\text{subject to}\quad \sum_{j=1}^n a_{ij}x_j \le b_i\ (i=1,\dots,m),\qquad x_j \ge 0\ (j=1,\dots,n).$$

A solution $x$ is feasible if it satisfies every constraint, and optimal if in addition it maximizes the objective among feasible solutions. The problem is infeasible if no feasible solution exists, and unbounded if it has feasible solutions with arbitrarily large objective values.

The slack variables $w_i = b_i - \sum_j a_{ij}x_j$ are appended to the list of variables as $x_{n+i} = w_i$, so that the constraints become the linear system $[A\ I]\,x = b$ with $x \ge 0$ in $\mathbb{R}^{n+m}$. A dictionary is given by a set $\mathcal B$ of $m$ basic indices whose columns of $[A\ I]$ are linearly independent; the remaining indices $\mathcal N$ are nonbasic. Solving for the basic variables gives

$$\zeta = \bar\zeta + \sum_{j\in\mathcal N}\bar c_j x_j,\qquad x_i = \bar b_i - \sum_{j\in\mathcal N}\bar a_{ij}x_j\quad (i\in\mathcal B).$$

The basic solution of the dictionary sets the nonbasic variables to zero. The dictionary is feasible if $\bar b_i \ge 0$ for every $i\in\mathcal B$, and degenerate if $\bar b_i = 0$ for some $i\in\mathcal B$.

The simplex method (Phase II) starts at a feasible dictionary and repeats a pivot: an entering variable $x_k$ is chosen among the nonbasic variables with $\bar c_k > 0$, and a leaving variable $x_l$ among the basic variables with $\bar a_{lk} > 0$ that minimize the ratio $\bar b_l/\bar a_{lk}$; then $x_k$ becomes basic and $x_l$ nonbasic. The method stops when no $\bar c_j$ is positive (the dictionary is optimal) or when the entering column has no positive $\bar a_{ik}$ (the problem is unbounded). A pivoting rule resolves the remaining choices. Bland's rule chooses both the entering and the leaving variable as the candidate with the smallest index. The lexicographic rule perturbs the right-hand sides by symbols $0<\epsilon_m\ll\dots\ll\epsilon_1\ll$ all data and chooses the leaving variable by the perturbed ratio test.

Formalization targets

Goal: Theorem 3.3 (termination under Bland's rule, p. 31)

From every feasible dictionary $D_0$, there is no infinite sequence of pivots

$$D_0\to D_1\to D_2\to\cdots$$

in which both the entering and the leaving variable follow Bland's rule; and a finite sequence of such pivots reaches a dictionary $D_T$ at which the method stops, optimal or exhibiting unboundedness.

Milestones

• Theorem 3.1 (p. 27): if the simplex method fails to terminate, it must cycle, i.e. an infinite run visits some dictionary twice.
• Theorem 3.2 (p. 30): the simplex method always terminates when the leaving variable is selected by the lexicographic rule.
• Theorem 3.4 (p. 33), the fundamental theorem: (1) with no optimal solution the problem is infeasible or unbounded; (2) if a feasible solution exists, a basic feasible solution exists; (3) if an optimal solution exists, a basic optimal solution exists.

Significance

The result. Termination under Bland's rule is what turns the simplex method from a heuristic into an algorithm. Combined with Phase I, it yields the fundamental theorem of linear programming, which reduces the search for an optimum to finitely many basic solutions and underlies the duality theory of the following chapters. Bland's rule also needs no perturbation or extra bookkeeping, and it is the anticycling rule used in many correctness proofs of simplex-type and combinatorial pivoting algorithms, including oriented-matroid programming.

Formalizing it. All four theorems are classical and proved. The Prove2Me library has the lexicographic rule and a nondegenerate termination theorem in the tableau setting of Bertsimas and Tsitsiklis (equality form $Ax=b$, $x\ge 0$, full row rank), and the existence of basic feasible and optimal solutions in that form. It has no statement of Bland's theorem, and none of Vanderbei's dictionary formulation over $[A\ I]$. This mission produces a machine-checkable model of dictionaries and pivoting rules in that formulation, and targets Bland's theorem, whose proof is a genuine combinatorial argument rather than a monotonicity argument.

Difficulty

The natural argument for termination is monotonicity: each pivot increases the objective, so no dictionary repeats. It fails exactly at degenerate pivots, where the step length $\bar b_l/\bar a_{lk}$ is zero and the objective and the basic solution do not change. Bland's rule gives no potential function that strictly increases along degenerate pivots, so the proof has to reason about a hypothetical cycle as a whole: which variables enter and leave the basis within it, and how two dictionaries of the cycle, in which the same variable leaves and later enters, constrain each other's coefficients. Relating the coefficients of two different dictionaries of the same problem is the step that has no counterpart in the model's definitions and has to be developed.

For Theorem 3.2, the symbols $\epsilon_i$ cannot be replaced by a fixed small real number: the method treats them as formal quantities on separate scales, and the statement is about that symbolic rule.

Formalization scope

Vectors are Fin n → ℝ, Fin m → ℝ, and the constraint matrix is Matrix (Fin m) (Fin n) ℝ. The $n+m$ variables are indexed by Fin (n + m) with the decision variables first and the slacks after them, which is the order $x_1,\dots,x_n,x_{n+1}=w_1,\dots,x_{n+m}=w_m$ that Bland's rule compares. A dictionary is a structure holding its basic set, a proof that it has $m$ elements and a proof that its columns of $[A\ I]$ are linearly independent; the coefficients $\bar b,\bar a,\bar c,\bar\zeta$ are computed as coordinates in the basis of basic columns. A dictionary is therefore determined by its basic set, as the proof of Theorem 3.1 uses. "Basic solution" is defined through such a dictionary, not as a support condition.

Termination is stated as the nonexistence of an infinite run from a feasible dictionary, for Theorems 3.2 and 3.3. The goal adds that a finite Bland run reaches a stopping dictionary, so that it cannot hold because pivots fail to exist. The lexicographic rule is encoded by lexicographic comparison of the coefficient vectors $(\bar b_i, r_{i1},\dots,r_{im})/\bar a_{ik}$ of the perturbed ratios; the symbol $\epsilon_p$ is attached in the starting dictionary to its $p$-th basic variable in increasing index order, which for the initial dictionary is the $p$-th constraint. Unboundedness in Theorem 3.4 is "for every $M$ a feasible solution with objective $>M$", as defined on p. 7. The statements carry no explicit constants.

A formalization that stated Theorem 3.3 for arbitrary pivot sequences with pairwise distinct bases would be Theorem 3.1's counting argument, not Bland's theorem; the goal is stated for pivots that follow Bland's rule and only those.

A complete development needs: the pivot update of a dictionary and the invariance of the solution set under it, feasibility preservation by the ratio test, the relation between the objective rows of two dictionaries, and finiteness of the set of bases. These are reusable for any later formalization of simplex-type algorithms. Proofs of the milestones, alternative proofs of Theorem 3.3, and Phase I (to connect Theorem 3.4 with the algorithm) are welcome.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 3. https://doi.org/10.1007/978-1-4614-7630-6
• R. G. Bland, New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2):103–107, 1977. https://doi.org/10.1287/moor.2.2.103
• G. B. Dantzig, A. Orden, P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2):183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
• E. M. L. Beale, Cycling in the dual simplex algorithm, Naval Research Logistics Quarterly 2(4):269–275, 1955. https://doi.org/10.1002/nav.3800020406
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.4 (lexicographic rule and Bland's rule in tableau form).

Motivation

The subgradient method for a nonsmooth convex function converges, but slowly: when the level sets of the objective are elongated, the subgradient is nearly orthogonal to the direction towards the minimum, and the method zigzags. For smooth functions the remedy is a change of metric (Newton and quasi-Newton methods); for nonsmooth functions no Hessian exists to supply one. N. Z. Shor's answer was to learn a metric from the subgradients themselves: after each step, stretch the space along the latest (transformed) subgradient, so that components of future subgradients parallel to it are damped. These subgradient methods with space dilation along the gradient (SDG methods) are the ancestors of Shor's r-algorithm and of the ellipsoid method, which the book (p. 49) describes as a special case of the same family and which Khachiyan later used to show that linear programming is solvable in polynomial time.

Section 3.4 of Shor's monograph (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński, doi:10.1007/978-3-642-82118-9) proves that, under a two-sided condition on the objective, a suitable SDG method decreases function values at the speed of a geometric progression whose ratio is invariant under nonsingular linear changes of variables. This mission formalizes that chain of results.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x,y)$. For a unit vector $\xi$ and a coefficient $\alpha \ge 0$, the operator of space dilation along $\xi$ is

$$R_\alpha(\xi)\,x = x + (\alpha - 1)(x,\xi)\,\xi ,$$

which multiplies the component of $x$ along $\xi$ by $\alpha$ and leaves the orthogonal complement fixed.

Let $f : E_n \to \mathbb{R}$ and let $g : E_n \to E_n$ be a generalized gradient: a subgradient of $f$ when $f$ is convex, an almost-gradient when $f$ is almost differentiable. The SDG method starts from $x_0$ and a nonsingular operator $B_0 = A_0^{-1}$. At step $k = 0, 1, \dots$: if $g(x_k) = 0$ it stops; otherwise it forms the transformed gradient $\tilde g_k = B_k^* g(x_k)$, the direction $\xi_{k+1} = \tilde g_k/\|\tilde g_k\|$, and

$$x_{k+1} = x_k - h_{k+1} B_k \xi_{k+1}, \qquad B_{k+1} = B_k R_{1/\alpha_{k+1}}(\xi_{k+1}), \qquad A_{k+1} = R_{\alpha_{k+1}}(\xi_{k+1}) A_k ,$$

with a stepsize $h_{k+1}$ and a dilation coefficient $\alpha_{k+1}$. So $A_k$ is the accumulated space transformation, $B_k = A_k^{-1}$, and each step is a subgradient step for $\varphi_k(y) = f(B_k y)$ in the variables $y = A_k x$.

The quantitative results assume, for a point $x^*$ and the ball $S_d = \{x : \|x - x^*\| \le d\}$, the two-sided condition

$$N\,[f(x) - f(x^*)] \le (g(x),\, x - x^*) \le M\,[f(x) - f(x^*)], \qquad x \in S_d, \quad M > N > 0. \qquad (3.18)$$

For a convex function the lower inequality holds with $N = 1$; the upper one bounds how far $f$ is from a positively homogeneous function around $x^*$.

Formalization targets

Goal: Theorem 3.4

Under (3.18), with $B_0 = I$, $x_0 \in S_d$, stepsizes $h_{k+1} = \frac{2MN}{M+N}\frac{f(x_k)-f(x^*)}{\|\tilde g_k\|}$, a constant coefficient $1 < \alpha \le \frac{M+N}{M-N}$, and $G$ a bound for $\|g\|$ on $S_d$: there are $c > 0$ and indices $k_1 < k_2 < \cdots$ with

$$f(x_{k_p}) - f(x^*) \le c\,\alpha^{-k_p/n},$$

and for every $k \ge 1$

$$\min_{0 \le i \le k-1}\,[f(x_i) - f(x^*)] \le \frac{G\sqrt{k(\alpha^2-1)}\,d}{N\sqrt{\alpha^{2k/n}-1}} .$$

Milestones

1. Eq. (3.4): $\|R_\alpha(\xi)x\| = \sqrt{\|x\|^2 + (\alpha^2-1)(x,\xi)^2}$.
2. Theorem 3.1: if $\|g(x_k)\| \le d$ and $1+\delta \le \alpha_k \le \alpha^*$, then $\|\tilde g_{k_p}\| < c\,(\prod_{j\le k_p}\alpha_j)^{-1/n}$ along a subsequence.
3. Theorem 3.2: for constant $\alpha > 1$ and $B_0 = I$, $\min_{0\le r\le k-1}\|\tilde g_r\| \le d\sqrt{k(\alpha^2-1)}/\sqrt{\alpha^{2k/n}-1}$.
4. Theorem 3.3: under (3.18) and the rules above, $\|A_k(x_k - x^*)\| \le d$ for all $k$.

Significance

The result shows that one fixed rule, depending only on $M$, $N$ and $n$, yields linear convergence of function values for every objective satisfying (3.18), at a ratio $\alpha^{-1/n}$ that does not deteriorate when the problem is badly scaled: the method, and hence its rate, is invariant under nonsingular linear changes of variables. This is the property the ellipsoid method inherits (Section 3.8 of the book), and the same space-dilation machinery drives the r-algorithm (Section 3.7), still used for large nonsmooth problems such as Lagrangian duals of integer programs.

The theorems are proved in the book; none of them, and no space-dilation method, has a machine-checked proof to our knowledge, and the platform has no statement about variable-metric subgradient methods. The mission provides a reusable formal model of the SDG iteration, the eigenvalue-growth arguments behind Theorems 3.1–3.2, and the one-step invariant of Theorem 3.3. The formalization also corrects two points of the printed text (see Formalization scope).

Difficulty

Theorem 3.3 is a one-step computation, but Theorems 3.1 and 3.2 are not: they relate the size of the transformed gradients to the growth of the singular values of $A_k$, whose determinant is $\prod_j \alpha_j$. A bound on $\|\tilde g_k\|$ at a single step says nothing, since the dilations can concentrate in few directions; the argument has to control the largest singular value of $A_k$ over many steps against the geometric-mean lower bound $(\det A_k)^{1/n}$. The dimension $n$ enters the rate exactly through this comparison. Theorem 3.4 then needs the invariant of Theorem 3.3 to keep every iterate inside $S_d$, where (3.18) and the bound $G$ are available.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ in the rate statements. Operators are continuous linear maps; $B_0$ is a continuous linear equivalence and $A_0$ its inverse. The state $(x_k, B_k, A_k)$ is produced by a defined recursion sdg, not assumed; $\tilde g_k$ is gTilde.
• The stepsize rule receives the index, the current point and $\tilde g_k$; the dilation coefficient at step $k$ is α (k+1). When $g(x_k) = 0$ the state is repeated, which encodes the book's stop; no division by zero is used.
• The book states Theorems 3.1–3.4 for almost differentiable $f$ with $g$ an almost-gradient; the proofs use only the bounds on $\|g\|$ and (3.18), so the Lean statements quantify over every map $g$ with those properties. $G$ is any bound for $\|g\|$ on $S_d$ in place of the maximum.
• Theorems 3.2–3.4 take $B_0 = I$, as their proofs do; Theorem 3.1 allows any nonsingular $B_0$.
• Two corrections to the printed statements, both following the proofs: Theorem 3.4's record bound carries the factor $1/N$ that the proof derives, and the record minima in Theorems 3.2 and 3.4 range over the indices $0, \dots, k-1$ that the proof controls, rather than $1, \dots, k$.
• Constants $c$ and subsequences are existential and chosen after the data of the run, before the index $p$. A statement placing $c$ after $p$, or dropping (3.18) on $S_d$, would be trivially true or false and is ruled out.

Useful infrastructure, reusable for the r-algorithm and ellipsoid chapters: identities for $R_\alpha(\xi)$, determinants and singular values of products of rank-one dilations, and the invariance of the SDG iteration under a linear change of variables. Proofs of any milestone, and alternative arguments for Theorem 3.1, are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§3.2–3.4, pp. 49–62 (translated by K. C. Kiwiel and A. Ruszczyński). https://doi.org/10.1007/978-3-642-82118-9

Motivation

Many optimization problems in operations research have objectives that are convex but not differentiable: the maximum of finitely many linear or smooth functions, the value function of a Lagrangian dual, the cost of a two-stage linear program as a function of the first-stage decision. Gradient methods do not apply to these directly. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer Series in Computational Mathematics 3, 1985; translated by K. C. Kiwiel and A. Ruszczyński from the 1979 Russian edition) develops the algorithms that replace the gradient by a subgradient, and its first chapter sets up the calculus of subgradients these algorithms rely on.

This mission is the first of a series formalizing the book. It covers §1.2 (convex functions and the concept of subgradient) and §1.3 (rules for computing subgradients), printed pages 7–16. Every later mission in the series (the subgradient method, space dilation, the ellipsoid method, decomposition) assumes that a subgradient of the objective can be computed, and §1.3 is where the book explains how: by combining subgradients of simpler pieces.

Setting

Write $E_n$ for $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. A function $f$ with domain a convex set $M \subseteq E_n$ is convex if its epigraph $\{(u, x) : u \ge f(x),\ x \in M\}$ is convex, equivalently $(1-\alpha) f(x_1) + \alpha f(x_2) \ge f((1-\alpha)x_1 + \alpha x_2)$ for $x_1, x_2 \in M$ and $\alpha \in [0,1]$.

Let $x_0$ be an interior point of $M$. A vector $g$ is a subgradient (or generalized gradient) of $f$ at $x_0$ if

$$f(x) - f(x_0) \ge (g, x - x_0) \qquad \text{for all } x \in M. \tag{1.3}$$

The set of all subgradients is the subdifferential, written $G(x_0)$ or $G_f(x_0)$. For $f$ differentiable at $x_0$ it is the single gradient; for $f(x) = |x|$ on $E_1$ it is $[-1, 1]$ at $x_0 = 0$.

The one-sided directional derivative of $f$ at $x_0$ in direction $\eta$ is

$$f'_\eta(x_0) = \lim_{t \to 0+} \frac{f(x_0 + t\eta) - f(x_0)}{t}.$$

A direction $\eta \ne 0$ is a direction of steepest descent at $x_0$ if $\min_{\|\xi\| = 1} f'_\xi(x_0) = f'_\eta(x_0)/\|\eta\|$.

Formalization targets

Goal: Theorem 1.12 (p. 13), the subdifferential of a nonnegative combination

For convex $f_1, \dots, f_k$ on $E_n$ and $a_1, \dots, a_k \ge 0$, the function $f = \sum_{i=1}^k a_i f_i$ is convex and, at every $x_0$,

$$G_f(x_0) = \Big\{ \sum_{i=1}^k a_i g_i \;:\; g_i \in G_{f_i}(x_0),\ i = 1, \dots, k \Big\}.$$

Both inclusions are part of the goal.

Milestones

1. Theorem 1.7 (p. 9): at an interior point $x_0$ of the domain, $G(x_0)$ is nonempty, bounded, convex and closed.
2. Theorem 1.8 (p. 9): at an interior point, $f'_\eta(x_0)$ exists for every $\eta$ and $f'_\eta(x_0) = \max_{g \in G(x_0)} (g, \eta)$, with the maximum attained.
3. Corollary (p. 12): an interior point $x_0$ minimizes $f$ on $M$ if and only if $0 \in G(x_0)$.
4. Theorem 1.11 (p. 12): if $0 \notin G(x_0)$ and $g_0$ is the element of $G(x_0)$ nearest the origin, then $-g_0$ is a direction of steepest descent.
5. Theorem 1.9 (p. 11): $f$ is convex on $E_n$ if and only if $f'_\eta(x)$ exists everywhere and $t \mapsto f'_\eta(x + t\eta)$ is nondecreasing for all $x, \eta$.
6. Theorem 1.10 (p. 11): a twice continuously differentiable $f$ is convex if and only if its Hessian is positive semidefinite everywhere.
7. Theorem 1.13 (p. 14): for convex $f_1, \dots, f_m$, the function $\varphi = \max_i f_i$ is convex and $G_{f_i}(x_0) \subseteq G_\varphi(x_0)$ for every index $i$ active at $x_0$.

Significance

The result. Theorem 1.12 is the finite-dimensional, finite-valued case of the Moreau–Rockafellar sum rule. With Theorem 1.13 it is the book's recipe for computing subgradients of functions assembled from simple pieces by nonnegative combinations and pointwise maxima, the two operations that produce most nonsmooth convex objectives in practice (Lagrangian duals, penalty functions, piecewise-linear costs). Theorem 1.8 identifies the directional derivative with the support function of the subdifferential; the Corollary and Theorem 1.11 give the optimality condition and the steepest-descent direction that every descent method for nonsmooth convex functions starts from.

Formalizing it. These results are classical and have been proved many times in textbooks (Rockafellar, Convex Analysis, 1970, §23). Mathlib at the pinned revision has convexity, separation theorems and Carathéodory's theorem, but no subdifferential of a convex function on $E_n$ and no max formula. The mission builds that layer: a subdifferential with the book's inequality (1.3), a one-sided directional derivative defined as a right-hand limit, and the calculus rules above. The platform has a Clarke-gradient analogue of Theorem 1.8 for locally Lipschitz functions and a Banach-space sum rule for $f + \tfrac12\|\cdot\|^2$; neither states the convex, finite-dimensional results here.

Difficulty

The inclusion "$\supseteq$" in Theorem 1.12 is immediate from (1.3). The inclusion "$\subseteq$" is the content: a subgradient of the sum is a global object, and nothing in (1.3) splits it into subgradients of the pieces. Adding the inequalities of the pieces only produces vectors of the right form; it does not show every subgradient of $f$ arises this way. Any argument has to use the finite dimension and the interior-point setting, which is where Theorems 1.7 and 1.8 (existence of subgradients, compactness of $G(x_0)$, existence of one-sided derivatives) come in.

Theorem 1.8 in turn needs the existence of a finite right-hand limit of the difference quotient, which requires both monotonicity of the quotient and a lower bound, and the existence of a subgradient attaining the maximum, which is a separation statement. Theorem 1.9's "if" direction must rebuild convexity from one-sided derivative information alone, with no differentiability assumption.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) and $(x, y)$ is inner ℝ x y. A function is f : EuclideanSpace ℝ (Fin n) → ℝ; the domain $M$ is a set, convexity on it is ConvexOn ℝ M f (which includes convexity of $M$), and interior points are x₀ ∈ interior M. Theorems 1.9, 1.10, 1.12 and 1.13 are stated on all of $E_n$ (Set.univ), as the book proves them.
• The subdifferential subdifferential M f x₀ is the set of $g$ with $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x \in M$. It is defined for any $x_0$; the interior-point assumption is a hypothesis of each theorem that needs it.
• HasOneSidedDirDeriv f x₀ η d is the right-hand limit Tendsto … (𝓝[>] 0) (𝓝 d), not Mathlib's two-sided lineDeriv. Maxima and minima are stated with IsGreatest/IsLeast (attained), never with sSup/sInf.
• Theorem 1.12 is an equality of sets over indices Fin k; $k = 0$ and zero coefficients are allowed, as in the book. Theorem 1.13's maximum is Finset.sup' over Fin m with $m \ge 1$, and it asserts only the inclusion the book states.
• Theorem 1.11 is stated as the book's proof establishes it: the steepest-descent direction is minus the minimal-norm subgradient. The printed statement names the minimal-norm subgradient itself, along which the directional derivative is positive.
• A formalization that states only "$\supseteq$" in Theorem 1.12, or only that each $\sum a_i g_i$ is a subgradient, is the easy half and does not count as the goal.
• Theorems 1.1–1.6 (supporting hyperplane, separation, representation by extremal points, the convexity inequality, continuity on the interior) are Mathlib-level (geometric_hahn_banach_*, Carathéodory and Krein–Milman, ConvexOn.continuousOn_interior) and are not restated.

Contributions welcome: proofs of any milestone, a reusable lemma that the difference quotient of a convex function is monotone in $t$, and a general max formula; these are reusable in the later missions of the series, which define subgradients the same way.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§1.2–1.3, pp. 7–16. https://doi.org/10.1007/978-3-642-82118-9
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §23 (subgradients) and Theorem 23.8 (sum rule). https://doi.org/10.1515/9781400873173
• J.-J. Moreau, "Fonctionnelles sous-différentiables", Comptes Rendus de l'Académie des Sciences 257 (1963), 4117–4119.

Motivation

Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states $\{0,1,\dots,N\}$ and hope that its value and its optimal policy approximate those of the original problem as $N$ grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC($\alpha$), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.

The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state $0$ is finite, yet a natural truncation produces values $V^N_\alpha(0)\ge \alpha N^2/((1-\alpha)[N(1-\alpha)+\alpha])\to\infty$. How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.

Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$; for each state $i$ a finite nonempty action set $A_i$; nonnegative finite costs $C(i,a)$; and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a)=1$. A policy $\theta$ chooses the action at time $t$ at random from a distribution $\theta(\cdot\mid h_t)$ on $A_{i_t}$ that may depend on the entire history $h_t=(i_0,a_0,\dots,i_{t-1},a_{t-1},i_t)$. A stationary policy $f$ always chooses $f(i)\in A_i$ in state $i$. Fix a discount factor $\alpha\in(0,1)$. The discounted cost of $\theta$ and the discounted value function are

$$V_{\theta,\alpha}(i)=\sum_{t\ge0}\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i],\qquad V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i),$$

both in $[0,\infty]$, the infimum over all policies. A policy is discount optimal if $V_{\theta,\alpha}=V_\alpha$.

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite nonempty sets $S_N$ increasing to $S$ and, for $i\in S_N$ and $a\in A_i$, probability distributions $P_{ij}(a;N)$ on $S_N$ with $P_{ij}(a;N)\to P_{ij}(a)$ as $N\to\infty$. The finite MDC $\Delta_N$ has state space $S_N$ and the same actions and costs; $V^N_\alpha$ is its value function and $f^N_\alpha$ a stationary policy attaining the minimum in its discount optimality equation

$$V^N_\alpha(i)=\min_{a\in A_i}\Big\{C(i,a)+\alpha\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)\Big\},\qquad i\in S_N.$$

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the excess probability $P_{ir}(a)$, $r\notin S_N$, according to augmentation distributions $q_j(i,a,r,N)$ on $S_N$: $P_{ij}(a;N)=P_{ij}(a)+\sum_{r\notin S_N}P_{ir}(a)q_j(i,a,r,N)$.

Assumption DC($\alpha$): for every $i\in S$, $W_\alpha(i):=\limsup_{N}V^N_\alpha(i)<\infty$ and $W_\alpha(i)\le V_\alpha(i)$.

Formalization targets

Goal: Theorem 4.6.3

The following are equivalent:

$$\text{(i)}\ \lim_{N\to\infty}V^N_\alpha(i)=V_\alpha(i)<\infty\ \ (i\in S);\qquad \text{(ii)}\ \text{Assumption DC}(\alpha).$$

Under either, every limit point of $(f^N_\alpha)_{N\ge N_0}$ (a stationary $f$ with $f^{N_r}(i)=f(i)$ eventually along a subsequence, for each $i$) is discount optimal for $\Delta$.

Milestones

• Lemma 4.6.2: $\liminf_N V^N_\alpha\ge V_\alpha$ for every approximating sequence.
• Proposition 4.7.1: bounded costs imply DC($\alpha$).
• Lemma 4.7.2: taboo probabilities of avoiding $S-S_N$ converge to the $t$-step transition probabilities.
• Lemma 4.7.3: for the first passage time $T_i(N)$ out of $S_N$ under a stationary policy, $E[\alpha^{T_i(N)}]\to0$.
• Proposition 4.7.4: if $V_\alpha<\infty$ and the ATAS sends excess probability to a finite set, DC($\alpha$) holds.
• Corollary 4.7.5: the case of a single distinguished state $z$, with the relative form of the optimality equation for $\Delta_N$.
• Proposition 4.7.6: if $V_\alpha<\infty$ and the augmentation distributions satisfy $\sum_{j\in S_N}q_j(i,a,r,N)v_{\alpha,n}(j)\le v_{\alpha,n}(r)$ for all $n\ge0$, then $V^N_\alpha\le V_\alpha$ on $S_N$.

Significance

Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.

All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and $[0,\infty]$-valued costs.

Difficulty

The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and $V_\alpha$ is only the minimal nonnegative solution of its optimality equation. Passing to the limit in $N$ inside $\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)$ is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing $\Delta_N$ with $\Delta$ along a coupled first passage out of $S_N$, which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding $V^N_\alpha$ by $\sup C/(1-\alpha)$ works only for bounded costs (Proposition 4.7.1).

Formalization scope

The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and $+\infty$ is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time $t$ is the $[0,\infty]$-valued sum over histories. $V_\alpha$ is the infimum over all such policies; a stationary policy enters as the policy putting mass one on $f(i)$. The discount factor is α : ℝ≥0 with $0<\alpha<1$ (the chapter's standing assumption). $\Delta_N$ is an MDC on the subtype $S_N$; $V^N_\alpha(i)$ is extended by $0$ when $N<N_0$ or $i\notin S_N$, a convention that affects finitely many $N$ for each fixed $i$ and hence no limit in $N$. Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity $E[\alpha^{T}]=\sum_{n\ge1}\alpha^nP(T=n)$ (so $\alpha^\infty=0$) are defined combinatorially from the transition probabilities.

A trivializing formalization is ruled out: $V_\alpha$ is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC($\alpha$) keeps both of its conditions, and statement (i) of the goal includes finiteness of $V_\alpha$.

A complete development needs the minimality of $V_\alpha$ among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Sections 4.6–4.7, pp. 73–81. https://doi.org/10.1002/9780470317037
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

The solution concept of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944) is defined from two ingredients: a set of imputations and a domination relation between them. A solution is a set of imputations that is internally stable (no member dominates another) and externally stable (every non-member is dominated by some member). In §65 of the book the authors observe that this definition never uses what imputations and domination actually are. They abstract it to an arbitrary set $D$ and an arbitrary relation $\mathcal S$ on $D$, and ask which properties of $\mathcal S$ guarantee that exactly one solution exists.

The abstract notion is what graph theory now calls a kernel of a directed graph: draw an arc $x \to y$ whenever $x\mathcal S y$; a solution is a set of vertices that is independent and absorbs every vertex outside it. Kernels appear in combinatorial game theory (the losing positions of a finite impartial game form a kernel of its move graph) and in the theory of preference and choice.

Timeline.

• 1944 (1st ed.; 3rd ed. 1953, reprinted 2007): von Neumann and Morgenstern define solutions for an arbitrary relation (§65), show that a finite set with an acyclic relation has exactly one solution (65:X), and that acyclicity is necessary for every subset to have a unique solution (65:Z).
• 1953: M. Richardson, Solutions of irreflexive relations, extends existence (not uniqueness) to finite relations without cycles of odd length.

Setting

Let $D$ be an arbitrary set and $\mathcal S$ an arbitrary relation on $D$; $x\mathcal S y$ is read "$x$ dominates $y$". A solution (in $D$ for $\mathcal S$) is a set $V \subseteq D$ with

$$\text{(65:1)}\qquad V = \{\, y \in D : x\mathcal S y \text{ holds for no } x \in V \,\}.$$

For $E \subseteq D$, an element $x$ is a maximum of $E$ if $x \in E$ and no $y \in E$ has $y\mathcal S x$; the set of maxima is $E^m$.

For $m \ge 1$, condition $(A_m)$ says: never $x_1\mathcal S x_0, x_2\mathcal S x_1, \dots, x_m\mathcal S x_{m-1}$ with $x_0 = x_m$ and all $x_i \in D$. The relation is acyclic if it satisfies every $(A_m)$, $m = 1, 2, \dots$; in particular never $x\mathcal S x$. It is strictly acyclic if there is no infinite sequence $x_0, x_1, x_2, \dots$ in $D$ with $x_{i+1}\mathcal S x_i$ for every $i$. Property (65:K) says that every non-empty $E \subseteq D$ has $E^m \ne \ominus$. A partial ordering (65:B) is a transitive relation for which at most one of $x = y$, $x\mathcal S y$, $y\mathcal S x$ holds.

For the main theorem the book constructs a candidate solution by induction (65.7.1): $A_1 = D$; $B_i = A_i^m$; $C_i$ is the set of elements of $A_i$ dominated by some element of $B_i$; $A_{i+1} = A_i - B_i - C_i$. With $i_0$ the first index for which $A_{i_0} = \ominus$,

$$\text{(65:2)}\qquad V_0 = B_1 \cup \cdots \cup B_{i_0 - 1}.$$

In Lean the elements live in a type α, D V : Set α, and S : α → α → Prop with S x y meaning $x\mathcal S y$; the predicates are IsSolution D S V, maxima E S, IsAcyclic, IsStrictlyAcyclic, HasMaximaProperty, IsPartialOrdering, ConditionG, and the construction stageA, stageB, stageC, V0.

Formalization targets

Goal: (65:X)

If $D$ is finite and $\mathcal S$ is acyclic on $D$, then

$$\exists!\, V:\ V \text{ is a solution in } D \text{ for } \mathcal S, \qquad\text{and}\qquad V \text{ is a solution} \iff V = V_0 .$$

Milestones, in attack order

1. (65:I) For a partial ordering, a finite $D$ satisfies (65:G): every non-maximal $y$ is dominated by some maximum.
2. (65:H) For a partial ordering of an arbitrary $D$: $V$ is a solution $\iff$ (65:G) holds and $V = D^m$.
3. (65:O:c) Strict acyclicity implies acyclicity; for finite $D$ the two are equivalent.
4. (65:P) (65:K) $\iff$ strict acyclicity, for arbitrary $D$.
5. (65:S) For finite $D$ and acyclic $\mathcal S$, some $A_i$ is empty.
6. (65:V) For finite $D$ and acyclic $\mathcal S$, every solution equals $V_0$.
7. (65:W) For finite $D$ and acyclic $\mathcal S$, $V_0$ is a solution.
8. (65:Z) If every $E \subseteq D$ has a unique solution in $E$ for $\mathcal S$, then $\mathcal S$ is acyclic on $D$.

Significance

The result itself. (65:X) is the most general of the book's three existence-and-uniqueness theorems for solutions (complete ordering, partial ordering, acyclic relation; 65.8.1). For games proper it has no direct application: the set of imputations of an essential game has no maxima, so (65:K) fails (65.9.1). Its role is to isolate a sufficient condition for a unique solution. With (65:Z), and applied to every subset of $D$, it characterizes the finite relations for which every subset has exactly one solution: exactly the acyclic ones (65.8.2). In graph language it is the statement that a finite directed acyclic graph has exactly one kernel. In combinatorial game theory this is the partition of the positions of a finite impartial game into P- and N-positions. The complete- and partial-ordering results (65:E)–(65:I) are the special cases the book treats first.

Formalizing it. The results are classical and fully proved in the book; to the best of our knowledge none of them is on the Prove2Me platform, and Mathlib has well-foundedness (WellFounded, RelEmbedding of ℕ) but no kernel or von Neumann–Morgenstern solution notion for an abstract relation. The mission produces machine-checked proofs of the book's §65 chain: the equivalence of (65:K) with strict acyclicity for arbitrary sets, the finite equivalence of acyclicity and strict acyclicity, the explicit construction of $V_0$, and the characterization of 65.8.2.

Difficulty

Most of the individual steps are short. The work is in making the book's finite induction precise. The sets $A_i$ are defined recursively and $V_0$ refers to the first empty stage $i_0$. The uniqueness proof (65:V) is a minimal-counterexample argument over the stage index, which moves between "smallest $k$ with $y \notin A_k$" and the disjoint decomposition (65:U) of $D$ into the $B_i$ and $C_i$. A tempting shortcut, taking an arbitrary well-founded rank function instead of the book's construction, proves existence and uniqueness but not that the solution is the $V_0$ of (65:2), which is part of the goal. For (65:P) and (65:O:c) the difficulty is the passage between finite cycles and infinite chains. Going from a chain in a finite set to a repetition needs a pigeonhole argument, and going from a set without maxima to a chain needs dependent choice.

Formalization scope

• Representation. An ambient type α; D, E, V are Set α; the relation is S : α → α → Prop and is only ever consulted on elements of the set under consideration, so it is the book's relation on $D$ (or its restriction to $E$). Finite and infinite sequences are functions ℕ → α.
• Solutions. IsSolution D S V is the set equation (65:1) literally; it forces $V \subseteq D$. Uniqueness in the goal is ∃! over all V : Set α, not over a subtype; there is no degenerate reading in which the solution is fixed by construction.
• Acyclicity. IsAcyclic D S requires $(A_m)$ for every $m \ge 1$, all cycle elements in $D$. The case $m = 0$ is excluded, as in the book (it would be unsatisfiable). This is equivalent to the absence of a Relation.TransGen loop inside $D$, but the book's form is stated.
• Construction. Stages are indexed from $0$: stageA D S k is the book's $A_{k+1}$. V0 D S is the union of all $B_i$, which equals $B_1 \cup \cdots \cup B_{i_0 - 1}$ because every later $B_i$ is empty.
• Standing hypotheses instantiated. (65:S), (65:V), (65:W) and the goal (65:X) carry the hypotheses of 65.7.1, "$D$ finite and $\mathcal S$ acyclic" (for finite $D$ equivalently strictly acyclic, i.e. (65:K)), as D.Finite and IsAcyclic D S. (65:H) and (65:I) carry the partial-ordering hypothesis (65:B:a), (65:B:b) of 65.5.1, and (65:I) also finiteness of $D$. (65:O:c), (65:P) and (65:Z) are for arbitrary $D$ and $\mathcal S$, as 65.6.2 and 65.8.2 state. The empty $D$ is allowed everywhere; there the unique solution is $\ominus$.
• Not stated. The infinite case of (65:X) and of (65:Y), which the book leaves open (65.7.1, 65.8.3, question (65:9)); the complete-ordering results (65:E), (65:F), which silently assume $D \neq \ominus$; the counting statement (65:8).
• Needed infrastructure. Finite-set induction and pigeonhole on Set.Finite, dependent choice for (65:P). The definitions are reusable for any later work on kernels of digraphs and on abstract stable sets. Proofs of any milestone, and alternative proofs of the goal, are welcome.

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §65, pp. 587–602. https://doi.org/10.1515/9781400829460
• M. Richardson, Solutions of irreflexive relations, Annals of Mathematics 58 (1953), 573–590. https://doi.org/10.2307/1969755

Motivation

The theory of Theory of Games and Economic Behavior (von Neumann and Morgenstern, 1944; 3rd ed. 1953) rests on one object: the characteristic function $v(S)$, the amount a coalition $S$ of players can secure for itself whatever the other players do. For zero-sum $n$-person games, Chapter VI defines $v(S)$ and proves (25.3.1 and 26.1.1) that the set functions arising this way are exactly those with $v(\emptyset)=0$, $v(-S)=-v(S)$ and superadditivity. Economic applications, however, are rarely zero-sum: exchange and production create value. Chapter XI extends the theory to general (non-zero-sum) games by adding a fictitious player who absorbs the total gain, and §57 answers the question that decides the scope of this extension: which set functions are characteristic functions of general games?

The answer, that these are exactly the superadditive set functions vanishing on the empty set, is the reason why the cooperative game theory that followed could take "a superadditive $v$ with $v(\emptyset)=0$" as its primitive object, usually without any underlying strategic game.

Setting

A general $n$-person game $\Gamma$ in normalized form has players $I=\{1,\dots,n\}$. Player $k$ chooses $\tau_k\in\{1,\dots,\beta_k\}$ with $\beta_k\ge 1$, without knowing the choices of the others, and receives the real amount $\mathcal H_k(\tau_1,\dots,\tau_n)$. No condition is imposed on $\sum_k\mathcal H_k$. The game is zero-sum if $\sum_{k=1}^n\mathcal H_k\equiv 0$.

The zero-sum extension $\overline\Gamma$ (56.2.2) adds a fictitious player $n+1$, who has no move and receives

$$\mathcal H_{n+1}(\tau_1,\dots,\tau_n)=-\sum_{k=1}^n\mathcal H_k(\tau_1,\dots,\tau_n).$$

Write $\overline I=\{1,\dots,n,n+1\}$. For $S\subseteq\overline I$, the coalition $S$ and its complement $\bot S=\overline I-S$ play a zero-sum two-person game. The pure strategies of $S$ are the tuples of choices of its real members. A mixed strategy $\xi$ of $S$ is a single probability distribution over these tuples, so the members of a coalition randomize jointly, and likewise $\eta$ for $\bot S$. The payoff to $S$ is $\sum_{k\in S}\mathcal H_k$. Then

$$v(S)=\max_\xi\min_\eta K(\xi,\eta),$$

where $K$ is the expected payoff to $S$. The function $v$ on all $S\subseteq\overline I$ is the extended characteristic function; its restriction to $S\subseteq I$ is the restricted characteristic function (57.1). For a zero-sum game the restricted function is the characteristic function of Chapter VI.

Formalization targets

Goal: 57.3.4

For every $n$ and every set function $v$ on the subsets of $I$,

$$v \text{ is the restricted characteristic function of some general game} \iff v(\emptyset)=0 \text{ and } v(S\cup T)\ge v(S)+v(T) \text{ for } S\cap T=\emptyset,$$

and for every set function $v$ on the subsets of $\overline I$,

$$v \text{ is the extended characteristic function of some general game} \iff v(\emptyset)=0,\ v(\bot S)=-v(S),\ v \text{ superadditive}.$$

In each direction a single game realizes $v$ on every set simultaneously; $v(I)$ is not constrained.

Milestones

1. (57:1:a)–(57:1:c): necessity of the extended conditions.
2. (57:2:a), (57:2:c), (57:2:b): necessity of the restricted conditions, including $v(-S)\le v(I)-v(S)$.
3. 57.3.1: sufficiency of (57:2:a), (57:2:c).
4. 57.3.3: sufficiency of (57:1:a)–(57:1:c).
5. (57:G): for such $v$, $v(-S)=-v(S)$ for all $S$ holds iff $v(S)+v(-S)=v(I)$ for all $S$ and $v(I)=0$.
6. (57:B): in a zero-sum game every one-element set of players is removable, meaning that some zero-sum game with the same characteristic function has payoffs that do not depend on that player's choice.
7. (57:C): the set of all players is removable iff the game is inessential, i.e. $v(S)=\sum_{k\in S}\alpha_k$.

Significance

The characterization fixes the domain of Chapter XI: every statement about solutions of general games is, by 57.3.4, a statement about superadditive set functions with $v(\emptyset)=0$, and conversely every such function is attained by a strategic game. That converse justifies studying cooperative games abstractly. (57:G) separates the zero-sum and constant-sum subclasses inside this domain. (57:B) and (57:C) quantify how much of a player's strategic role survives when his moves are removed, which is the book's justification for the fictitious player.

Status: all results are proved in the book (1944). To our knowledge none of them is machine-checked; the Prove2Me catalog has superadditive and convex cooperative games, but none tied to a strategic game, and no characteristic function built from a minimax value. The work here is formalizing the known proofs.

Difficulty

Necessity reduces to the zero-sum theory applied to $\overline\Gamma$, but still requires the minimax theorem for the coalition's two-person game and a careful treatment of joint mixing when two disjoint coalitions merge. Sufficiency requires building one finite game whose coalition values equal an arbitrary superadditive $v$ exactly, for all $2^n$ coalitions at once. The obvious attempt, choosing payoffs coalition by coalition, fails because the payoffs are shared: a construction that gives $S$ the right value can change the value of every set that overlaps $S$. The difficulty is to obtain the upper bound $v(S)\le v_0(S)$ for every $S$ simultaneously. For the extended function there is a further difficulty. The fictitious player has no move, so the values on sets containing $n+1$ are forced by the others, and they must be reconciled with (57:1:b).

For (57:B), the target game must reproduce an arbitrary zero-sum characteristic function while one prescribed player's choice has no effect on any payoff.

Formalization scope

Players are Fin n (book indices $1,\dots,n$ become $0,\dots,n-1$); sets of players are Finset (Fin n). The extended domain $\overline I$ is Fin (n + 1) with the fictitious player Fin.last n, and $\bot S$ is the complement in Fin (n + 1). A game (GeneralGame n) has $\beta_k\ge1$ strategies Fin (β k) per player and real payoffs; zero-sum is the predicate IsZeroSum. The fictitious player's single strategy is left out of the coalition's strategy tuples, which does not change the two-person game. Max and Min are ⨆/⨅ over Mathlib's stdSimplex on the coalition's strategy tuples (one joint distribution per coalition). Both simplices are nonempty and the payoff is bounded, so these are attained values and no junk value from an empty or unbounded supremum occurs.

Standing hypotheses and their instantiation:

• finite strategy sets with $\beta_k\ge1$ (11.2.3, 56.2.2): a field of GeneralGame;
• "always assuming (57:2:a), (57:2:c)" for (57:G) (p. 537): an explicit hypothesis;
• "zero-sum $n$-person game" in (57:A)–(57:C) (p. 533): the hypothesis Γ.IsZeroSum and the requirement that the replacement game $\Gamma'$ is zero-sum;
• "no influence upon the course of the game" (57:A): all payoffs are independent of that player's variable, as in the proof of (57:C) on p. 534;
• "inessential" (57:C): the additive form (57:13), which p. 534 calls "precisely the definition of inessentiality".

No normalization is imposed: $v(I)$ is arbitrary and nothing is reduced. Every statement is made for all $n\ge0$; the book's $n\ge1$ is not needed, so this is a strengthening.

A trivializing formalization is ruled out: the characteristic function is defined from the game through the coalition's minimax value, so it is never a free parameter, and the existence claims must produce one game for all coalitions at once.

Needed infrastructure: finite zero-sum two-person games with joint mixed strategies over dependent product types; the minimax theorem ((17:6), on the platform as AGT.zero_sum_minimax for matrices); and product decompositions of coalition strategy tuples. The coalition-value API is reusable for any mission built on characteristic functions (Chapters VI, IX–XI). Contributions of this API as separate lemmas are welcome.

Not stated: (57:E*), (57:F*) (given without proof on p. 535), the open question (57:D), and (57:H), because the notion of a "dummy" it uses (from 46.9 and 56.3) is not defined on these pages.

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §§56–57, pp. 504–537. https://doi.org/10.1515/9781400829460
• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847