Operations Research

Why airlines protect seats

An airline sells the seats of one flight in several fare classes at different prices, all drawn from one shared cabin. Discount fares are bought early, under advance-purchase restrictions, while most high-fare requests arrive close to departure. Accepting every early low-fare request fills the aircraft with cheap passengers and turns away late high-fare passengers; refusing too many leaves seats empty. Seat inventory control decides how many seats to keep away from the low fare. Peter Belobaba's 1987 MIT thesis (Flight Transportation Laboratory Report R87-7) introduced the expected marginal seat revenue (EMSR) model for this decision, and EMSR-type rules remain the basis of the booking-limit logic in airline revenue management systems.

Timeline. Littlewood (1972, AGIFORS Symposium Proceedings; reprinted 2005) proposed accepting a low-fare request as long as its fare is at least the high fare times the probability of selling all remaining seats to high-fare passengers. Analysts at Trans World Airlines (1973) and Richter at Lufthansa (1982) gave equivalent formulations for the dynamic case. Belobaba (1987, Ch. 5) restated the two-class rule as a static protection level for nested inventories and extended it heuristically to many classes. Brumelle and McGill (Operations Research 41, 1993) and Curry (Transportation Science 24, 1990) later proved optimality of nested protection levels for any number of classes under low-to-high arrivals, and showed that Belobaba's multi-class EMSR levels are not optimal for three or more classes. This mission concerns only the two-class result, which is correct.

Setting

A single flight leg has capacity $C \in \mathbb N$. Class 1 has fare $f_1$, class 2 has fare $f_2$, with $0 \le f_2 \le f_1$. The numbers of requests for the two classes are random variables $r_1, r_2$ with values in $\mathbb N$, defined on a probability space $(\Omega, \mu)$ and independent. There are no cancellations, no no-shows, and a refused request is lost.

The inventory is nested: a class-1 request is accepted as long as any seat is unsold. A protection level $S \in \{0, \dots, C\}$ is the number of seats reserved for class 1; it sets the class-2 booking limit $BL_2 = C - S$. All class-2 requests arrive before any class-1 request. Class 2 therefore books $\min(r_2, C - S)$ seats and class 1 books $\min(r_1, C - \min(r_2, C-S))$, and the realised revenue is

$$R_S = f_2 \min(r_2, C - S) + f_1 \min\bigl(r_1,\, C - \min(r_2, C - S)\bigr).$$

The expected revenue is $\bar R(S) = \mathbb E[R_S]$.

The tail probability of class 1 is $\bar P_1(S) = P[r_1 \ge S]$, the probability of receiving $S$ or more class-1 requests, and the expected marginal seat revenue of the $S$-th class-1 seat is

$$\mathrm{EMSR}_1(S) = f_1 \cdot \bar P_1(S).$$

For a single class with $S$ seats the expected revenue is $f_1\,\mathbb E[\min(r_1, S)]$, and $\mathrm{EMSR}_1(S)$ is its increment from $S-1$ to $S$ seats. The EMSR protection level $S_2^1$ is the largest integer $S \in \{0, \dots, C\}$ with

$$\mathrm{EMSR}_1(S) \ge f_2 .$$

In Lean these objects are nestedRevenue, expectedNestedRevenue, tailProb, classRevenue, emsr and emsrProtectionLevel in SeatInventory.Nested.

Formalization targets

Goal: Eqs. (5.15)–(5.16), optimality of the EMSR protection level

$$\bar R(S) \le \bar R(S_2^1) \qquad \text{for all } S \in \{0, \dots, C\}.$$

The goal fixes no distribution: it holds for every pair of independent $\mathbb N$-valued demands, and $S_2^1$ depends only on $f_2/f_1$ and the law of $r_1$.

Milestones

1. Eq. (5.11). $f_1\mathbb E[\min(r_1,S)] - f_1\mathbb E[\min(r_1,S-1)] = f_1 P[r_1 \ge S]$ for $S \ge 1$.
2. Eqs. (6.1)–(6.2). $\bar P_1$ and, for $f_1 \ge 0$, $\mathrm{EMSR}_1$ are non-increasing in $S$.
3. Eq. (4.8), Littlewood's rule, already on the platform as RevenueManagement.littlewood_marginal_value (Talluri and van Ryzin's Eq. (2.1), proved).
4. Sect. 5.2, p. 112. $\bar R(S) \le \bar R(S_2^1)$ for $S_2^1 \le S \le C$: a smaller booking limit for class 2 cannot raise expected revenue.
5. Sect. 5.2, p. 114. With the same class-2 limit $C - S$, the expected nested revenue is at least the expected revenue of two distinct inventories with $S$ and $C - S$ seats, strictly if $f_1 > 0$ and $P[r_2 < C - S,\ r_1 > S] > 0$.

Significance

The two-class result says that, for a static booking limit set once before sales open and low-fare demand arriving first, the airline needs only the high-fare demand distribution and the fare ratio to set the optimal limit; the low-fare forecast is irrelevant. This is the rule that the thesis then applies class by class in multi-class nested systems, and it is the base case against which the later exact multi-class theory (Brumelle–McGill, Curry) is checked. Milestone 5 makes precise why nested inventories dominate the distinct-inventory allocation of the thesis's Sect. 5.1 with the same class-2 limit.

The result is classical and proved, in the sense that the optimality of a two-class threshold policy follows from Littlewood's argument and from the dynamic-programming treatment in Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004, Ch. 2). On Prove2Me, Littlewood's marginal rule and the dynamic-programming optimality of nested protection levels (RevenueManagement.static_optimal_controls) are formalized, but in Bellman form: there the protection level is defined through the value function of a dynamic program. What is not formalized is the statement in Belobaba's form, where the protection level is the explicit threshold of $f_1 P[r_1 \ge S]$ against $f_2$ and the objective is the explicit expected revenue of a booking limit. Connecting the two forms, and the comparison with distinct inventories, is the work of this mission.

Difficulty

The expected revenue couples the two demands through the capacity left by class 2, so $\bar R$ is not a sum of single-class revenues and is not separately concave in an obvious way. The step that requires care is the increment $\bar R(S) - \bar R(S-1)$: it is not $\mathrm{EMSR}_1(S) - f_2$, as the thesis's sentence after the milestone on p. 112 suggests, because the extra protected seat matters only on the event that class 2 would have reached its limit. Independence of $r_1$ and $r_2$ is what makes that event's probability factor out; without independence the threshold rule is not optimal. The discrete reading matters too: with $P[r_1 > S]$ in place of $P[r_1 \ge S]$ the rule is off by one seat and the claim fails.

Formalization scope

Conventions the Lean statements commit to:

• Demands are $\mathbb N$-valued measurable random variables r₁ r₂ : Ω → ℕ on a probability space μ; the goal and milestone 4 assume IndepFun r₁ r₂ μ. The thesis writes continuous densities (Eqs. (5.1)–(5.5)) but requires integer seat counts; the discrete model is used throughout.
• $\bar P_1(S) = P[r_1 \ge S]$, as in Eq. (6.2) and the prose of Eq. (5.11), not $P[r_1 > S]$ as in Eq. (5.2).
• The EMSR protection level is the largest $S \in \{0,\dots,C\}$ with $f_1 P[r_1 \ge S] \ge f_2$ (Eq. (5.15)); Eq. (5.16)'s equality is the continuous idealisation and is not stated.
• Booking order: all class-2 requests precede all class-1 requests (pp. 108, 112). This order is built into the revenue formula, not assumed separately.
• Fares satisfy $0 \le f_2 \le f_1$; the thesis has $f_1 > f_2$, and the statements also cover equality.
• Expectations are Bochner integrals of bounded revenues, probabilities are μ.real; seat counts use truncated subtraction only where $S \le C$.

A trivializing formalization is ruled out: $S_2^1$ is defined by the threshold of (5.15), never as an argmax of expected revenue, and the expected revenue is computed from the realised revenue of the booking process, not postulated as a sum of marginal terms.

The multi-class EMSR levels of Eqs. (5.19)–(5.29) and the dynamic revision of Eqs. (5.31)–(5.32) are out of scope. Proofs need the discrete expectation identity $\mathbb E[\min(r,S)] - \mathbb E[\min(r,S-1)] = P[r \ge S]$ and expectation of products of independent bounded functions, both in Mathlib's reach and reusable for other single-leg revenue models. Proofs of any milestone, and a proof of the goal from milestones 1, 2 and 4 plus the matching lower-half argument, are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• S. L. Brumelle and J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41, 1993. https://doi.org/10.1287/opre.41.1.127
• R. E. Curry, Optimal airline seat allocation with fare classes nested by origins and destinations, Transportation Science 24, 1990. https://doi.org/10.1287/trsc.24.3.193
• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Why airlines allocate seats by fare class

An airline sells the seats of one flight leg at several prices. Low fares fill seats that would otherwise fly empty; high fares are bought by passengers who book late and cannot be predicted exactly. Seat inventory control decides how many seats each fare class may sell. Peter Belobaba's 1987 MIT dissertation (MIT Flight Transportation Laboratory Report R87-7) gave the probabilistic treatment of this problem that became the expected marginal seat revenue (EMSR) method, which was in use across the airline industry for decades.

This mission formalizes the first, simplest model of the thesis: distinct (non-nested) fare-class inventories on a single leg, where a seat assigned to a class may be sold only in that class or not at all. The thesis surveys this model in Sect. 4.2 (pp. 84–94), where an integer-programming formulation from McDonnell-Douglas and its solution by ranking marginal values are described (p. 90), and develops it probabilistically in Sect. 5.1 (pp. 102–107).

Setting

A leg has capacity $n$ seats (the thesis also writes $C$). There are finitely many fare classes $i$. Class $i$ has an average fare $f_i \ge 0$ and receives a random number of requests $r_i \in \{0,1,2,\dots\}$, with law $p_i$. The seats are split into allocations $S_i \in \mathbb{N}$, one per class.

With $S$ seats, a class books requests until its seats run out, so its bookings and spill (refused requests) are

$$b = \min(r, S), \qquad l = (r - S)^+ \qquad \text{(Eq. (5.3))}.$$

The expected revenue of class $i$ is $\bar R_i(S_i) = f_i \cdot \bar b_i(S_i)$ with $\bar b_i(S_i) = E[\min(r_i,S_i)]$, and the leg's expected revenue is $\bar R = \sum_i \bar R_i(S_i)$ (Eq. (5.9)). Write

$$\bar P_i(S) = P[r_i \ge S], \qquad \mathrm{EMSR}_i(S) = f_i \cdot \bar P_i(S) \qquad \text{(Eqs. (5.11), (6.1), (6.2))},$$

the expected marginal seat revenue of the $S$-th seat of class $i$. The value of the $k$-th seat of class $i$ in the integer program of p. 90 is $m_i(k) = \mathrm{EMSR}_i(k)$, $k = 1, \dots, n$.

Formalization targets

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)

Let $T$ be any set of $n$ pairs $(i,k)$, $1 \le k \le n$, such that every $m_i(k)$ with $(i,k) \in T$ is at least every $m_j(l)$ with $(j,l) \notin T$, and let $S^T_i = \#\{k : (i,k) \in T\}$. Then $\sum_i S^T_i = n$ and

$$\sum_i f_i\, E[\min(r_i, S_i)] \;\le\; \sum_i f_i\, E[\min(r_i, S^T_i)] \qquad \text{for every } S \text{ with } \textstyle\sum_i S_i \le n .$$

The goal fixes no distribution, number of classes or fare ordering, and it holds for every tie-breaking among equal marginal values.

Milestones

1. Eq. (5.6): $\bar b_i(S) + \bar l_i(S) = \bar r_i$ for requests of finite mean.
2. Eq. (5.11): $\bar R_i(S) - \bar R_i(S-1) = f_i \cdot P[r_i \ge S]$ for $S \ge 1$.
3. Eqs. (6.1)–(6.2): $\bar P_i$ and $\mathrm{EMSR}_i$ are non-increasing in $S$.
4. Eq. (4.5): the 0–1 vector equal to $1$ on a set of $n$ largest $m_i(k)$ is an optimal solution of the linear program $\max \sum_{i,k} X_{ik} m_i(k)$ subject to $\sum X_{ik} \le n$, $0 \le X_{ik} \le 1$.
5. Eq. (5.13), discrete form: an allocation of exactly $C$ seats maximises $\bar R$ among such allocations if and only if some $\lambda$ satisfies $\mathrm{EMSR}_i(S_i) \ge \lambda$ whenever $S_i \ge 1$ and $\mathrm{EMSR}_i(S_i + 1) \le \lambda$, for all $i$.

Significance

The goal is the reason distinct-inventory allocation is computationally easy: a revenue-maximising allocation is obtained by sorting $n \times (\text{number of classes})$ numbers, with no search over allocations. The same marginal-value principle underlies the EMSR rules for nested classes in the rest of the thesis, and the identity (5.11) is the link between an expected-revenue function and its marginal seat values used throughout revenue management. Milestone 5 is the integer form of the Lagrangian condition of Eq. (5.13); the thesis states it only for a continuous relaxation, and its equality form is generally unattainable with integer seats.

These results are classical and their proofs are elementary; to our knowledge none of them has been machine-checked. The mission produces a reusable formal model of a single-leg, distinct-inventory allocation problem with integer demand (bookings, spill, revenue and marginal values of a PMF ℕ), and checked statements of the marginal-allocation principle for it.

Difficulty

The thesis argues with continuous densities and derivatives, setting $\partial \bar R / \partial S_i$ equal across classes. That argument does not transfer to integer seats: the derivative of a step-shaped expected-revenue function does not exist, equality of marginal values across classes generally fails at every integer allocation, and the tail probability must be $P[r \ge S]$ rather than the $P[r > S]$ of Eq. (5.2) for the marginal identity to hold. The integer statements need their own exchange argument. A second subtlety is ties: "the $n$ largest values" is not unique, and the goal must hold for every admissible choice, including choices in which a class's selected seat numbers are not an initial segment $\{1, \dots, S_i\}$.

Formalization scope

All declarations live in the namespace SeatInventory.Distinct. Conventions:

• Integer demand. The law of class $i$'s requests is d i : PMF ℕ; expectations are series over $\mathbb{N}$. The thesis's continuous densities are replaced by this discrete model, which the thesis itself requires for seat allocations (p. 103).
• Tail convention. $\bar P(S) = P[r \ge S]$, as in Eq. (6.2) and the prose of Eq. (5.11) ("the probability of selling $S_i$ or more seats"), not the $P[r > S]$ of Eq. (5.2).
• Seat numbers start at 1, and the pairs $(i,k)$ range over $k \in \{1, \dots, n\}$, as the 600 variables of a 150-seat, four-class problem on p. 90 indicate.
• Nonnegative fares $f_i \ge 0$ are assumed in every statement that needs them; with a negative fare the capacity constraint $\sum S_i \le n$ would not bind and the claims fail.
• Finite mean of the requests is assumed explicitly for Eq. (5.6); the thesis assumes it silently. Expected bookings are bounded and need no assumption.
• Capacity. The goal and the LP compare against allocations with $\sum_i S_i \le n$ (the LP's constraint); milestone 5 compares allocations of exactly $C$ seats (Eq. (5.8)).
• No independence assumption. Expected revenue of distinct inventories depends only on each class's marginal law, so the statements take one law per class.
• "Decreasing" is non-increasing. The thesis's justification in Sect. 6.1.1 gives only monotonicity; strict decrease fails for bounded demand.
• LP integrality. "The solution will be integer" is stated as: the indicator of every set of $n$ largest values is optimal. With ties the LP also has fractional optima.

The expected revenue in the goal is computed from the booking rule $\min(r_i, S_i)$; it is not defined as a sum of marginal values, and the optimal allocation is not defined as an argmax of $\bar R$. Either shortcut would make the goal a tautology and is ruled out.

Needed infrastructure: tail sums of a PMF ℕ, telescoping of $E[\min(r, S)]$, and a finite exchange argument for sums of the $n$ largest values of a function on a finite set; the last two are reusable for any separable concave resource-allocation problem. Contributions of proofs of any milestone, and of a verified sorting routine that produces a set of $n$ largest values, are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
• P. P. Belobaba, Airline yield management: an overview of seat inventory control, Transportation Science 21(2), 63–73, 1987. https://doi.org/10.1287/trsc.21.2.63
• P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134

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

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