Operations Research

Motivation

A two-person zero-sum stochastic game (also called a Markov game) is a Markov decision problem with two decision makers who pull in opposite directions: at every time point both players choose an action simultaneously, one player pays the other, and the system moves to a random next state whose law depends on the current state and both actions. Stochastic games were introduced by Shapley (Shapley 1953) and are the standard model for adversarial sequential decisions in operations research, economics and computer science (pursuit–evasion, inspection, robust control against an adversarial environment).

Shapley proved that a discounted stochastic game has a value and that both players have stationary optimal policies. The value, however, is in general not computable by linear programming: it need not lie in the field generated by the data. Kallenberg's Example 6.2.1 (after Parthasarathy and Raghavan) has rational data and an irrational value in one state. When only one player controls the transition probabilities, the situation changes: the value and stationary optimal policies are the optimal solutions of one pair of dual linear programs (Parthasarathy & Raghavan, as cited in Kallenberg 1983, pp. 192 and 196; Kallenberg 1983, Chapter 6).

Timeline.

• 1953: Shapley proves existence of the value and of stationary optimal policies for the discounted game.
• 1977–1978: Parthasarathy and Raghavan study games in which one player controls the transitions and identify an order-field property for the value and optimal decision rules (cited in Kallenberg 1983, pp. 192, 196).
• 1983: Kallenberg presents the dual pair (6.2.1)/(6.2.2), with the controlling player's policy read off the dual and the opponent's from the primal, and a constructive existence proof (Remark 6.2.2).

Setting

The state space is $E = \{1,\dots,N\}$ with $N>0$. In state $i$ player I chooses an action $a$ from a finite nonempty set $A(i)$ and player II an action $b$ from a finite nonempty set $B(i)$. Player I then receives $r_{iab}$ from player II, and the next state is $j$ with probability $p_{iabj} \ge 0$, where $\sum_j p_{iabj} \le 1$.

A history at time $t$ is $(i_1,a_1,b_1,\dots,i_{t-1},a_{t-1},b_{t-1},i_t)$. A policy $R_1$ of player I chooses, at each time and history, a probability distribution on $A(i_t)$; policies $R_2$ of player II are defined likewise. A policy is stationary, written $\pi^\infty$ or $\rho^\infty$, if the distribution depends only on the current state. With $v_i^t(R_1,R_2)$ the expected reward in period $t$ from initial state $i$, the total reward is $v_i(R_1,R_2) = \sum_{t\ge1} v_i^t(R_1,R_2)$.

A pair $(R_1^*,R_2^*)$ is optimal if, componentwise,

$$v(R_1,R_2^*) \le v(R_1^*,R_2^*) \le v(R_1^*,R_2) \qquad\text{for all policies } R_1,R_2, \tag{6.1.1}$$

and then $\mathrm{val(TMG)} := v(R_1^*,R_2^*)$ is the value of the game.

Assumption 6.2.1 (contraction). There are $\mu \gg 0$ and $\alpha\in[0,1)$ with $\sum_j p_{iabj}\mu_j \le \alpha\mu_i$ for all $i$, $a\in A(i)$, $b\in B(i)$. The discounted game is the case $\mu = e$.

Assumption 6.2.2 (single controller). $p_{iabj}$ does not depend on $b$; it is written $p_{iaj}$.

For a stationary $\rho$ write $r_{ia}(\rho) = \sum_b r_{iab}\rho_{ib}$ and $p_{iaj}(\rho)=\sum_b p_{iabj}\rho_{ib}$. A vector $y$ is TMG-superharmonic if some stationary $\rho^\infty$ of player II satisfies $y_i \ge r_{ia}(\rho) + \sum_j p_{iaj}(\rho) y_j$ for all $a\in A(i)$, $i\in E$. For weights $\beta_j>0$ the two linear programs are

$$\min\Big\{\textstyle\sum_j\beta_jy_j \ \Big|\ \sum_j(\delta_{ij}-p_{iaj})y_j-\sum_b r_{iab}\rho_{ib}\ge0;\ \sum_b\rho_{ib}=1;\ \rho_{ib}\ge0\Big\} \tag{6.2.1}$$ $$\max\Big\{\textstyle\sum_iz_i \ \Big|\ \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=\beta_j;\ -\sum_a r_{iab}x_{ia}+z_i\le0;\ x_{ia}\ge0\Big\} \tag{6.2.2}$$

Formalization targets

Goal: Theorem 6.2.3

Under Assumptions 6.2.1 and 6.2.2, let $(y^*,\rho^*)$ and $(x^*,z^*)$ be optimal solutions of (6.2.1) and (6.2.2), and $\pi^*_{ia} := x^*_{ia}/\sum_a x^*_{ia}$. Then

$$v(R_1,(\rho^*)^\infty) \le v((\pi^*)^\infty,(\rho^*)^\infty) = y^* \le v((\pi^*)^\infty,R_2)\qquad\text{for all policies } R_1,R_2 .$$

The goal fixes no constants; it states that the LP pair produces the value and optimal stationary policies.

Milestones

1. Theorem 6.2.1 (Shapley): under Assumption 6.2.1 both players have stationary optimal policies.
2. Theorem 6.2.2: under Assumption 6.2.1, $\mathrm{val(TMG)}$ is the smallest TMG-superharmonic vector.
3. Theorem 6.2.4 (i): for a stationary $\pi^\infty$ of player I, $x_{ia}(\pi) = [\beta^T(I-P(\pi))^{-1}]_i\pi_{ia}$ and $z_i(\pi) = \min_{b} r_{ib}(\pi)\sum_a x_{ia}(\pi)$ give a feasible point of (6.2.2) with $\sum_i z_i(\pi) = \min_\rho \sum_j\beta_j v_j(\pi^\infty,\rho^\infty)$.
4. Theorem 6.2.4 (ii): every feasible $(x,z)$ of (6.2.2) has $x = x(\pi)$ and $z\le z(\pi)$ for $\pi_{ia} = x_{ia}/\sum_a x_{ia}$.

Theorems 6.2.1 and 6.2.2 hold for the general contracting game. Assumption 6.2.2 enters only from (6.2.1) on.

Significance

The result. Theorem 6.2.3 turns a single-controller game into a finite computation, Algorithm XXVII: solve one LP pair and read off the value and optimal stationary policies of both players. A consequence (Remark 6.2.1) is that the value and the optimal decision rules lie in the field generated by the rewards and transition probabilities. Example 6.2.1 shows this fails without Assumption 6.2.2. Theorem 6.2.4 matches the feasible points of the dual program with the stationary policies of the controlling player. This is the game version of the correspondence between state-action frequencies and policies in Markov decision problems.

Formalizing it. All results are proved in the book, and Theorem 6.2.1 is classical. None of them is formalized: the platform has turn-based stochastic games with positional strategies (TBSGStrategyIteration), which do not cover simultaneous moves or history-dependent randomized policies. The mission adds a reusable model of simultaneous-move stochastic games with history-dependent policies, together with machine-checked optimality of the LP solution against every such policy.

Difficulty

There are two difficulties. First, optimality in (6.1.1) is against every history-dependent randomized policy of the opponent, while the LP produces only stationary policies. Fixing one player's stationary policy reduces the game to a Markov decision problem for the other player (Remark 6.1.1), and the facts needed from that problem (stationary policies suffice, and the value is the smallest superharmonic vector) are theorems about contracting MDPs, not consequences of the LP. Second, Theorem 6.2.2 rests on Shapley's existence theorem, which is not a linear-programming fact: its usual proof is a fixed-point argument for the Shapley operator built from one-stage matrix games. Remark 6.2.2 indicates a route that avoids it, through the bounded polytope of state-action frequencies of a contracting MDP. Either way, LP duality alone does not give optimality against non-stationary opponents.

Formalization scope

• Model. $E$ is Fin N with $N>0$. Actions live in finite types α, β, and $A(i)$, $B(i)$ are nonempty Finsets. Rows are substochastic.
• Policies. A history in $H_{n+1}$ is a record of $n+1$ states and $n$ actions of each player. A policy is a family of distributions indexed by time and history, supported on the current action set. Stationary policies are the image of state-dependent decision rules.
• Probabilities and reward. History probabilities are explicit finite products, with no measure theory. The total reward is the tsum of the period rewards, which converges absolutely under Assumption 6.2.1, and every theorem assumes it.
• Linear programs. Their variables are functions on all actions that vanish off $A(i)$ (resp. $B(i)$). Optimality means feasible and attaining the min/max over the feasible set. The common $p_{iaj}$ is $p_{iab_0j}$ for a fixed $b_0\in B(i)$, and Assumption 6.2.2 makes the choice irrelevant. $\beta_j>0$ is a hypothesis, as on p. 194.
• The minimum in Theorem 6.2.4 (i) is over stationary policies of player II and is stated with attainment.

Restricting either player's policy class to stationary policies would make the optimality claims of Theorems 6.2.1 and 6.2.3 a statement about a finite family and is ruled out: the comparison class is all history-dependent randomized policies.

Lemma 6.1.1 is Mathlib's isSaddlePointOn_value (Mathlib/Order/SaddlePoint.lean) and is not restated. The LP duality theorems of Chapter 1 are proved on the platform (LinearOptimization.lp_strong_duality, lp_complementary_slackness) and may be used. Useful contributions include: the reduction of Remark 6.1.1 (a fixed stationary opponent gives an MDP), the contracting-MDP facts it needs, and a proof of Theorem 6.2.1. The model definitions are reusable for any finite stochastic game.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 6. https://ir.cwi.nl/pub/13008
• L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
• T. Parthasarathy and T. E. S. Raghavan, Finite algorithms for stochastic games, International Conference on Dynamic Programming, Vancouver, 1977; cited in Kallenberg 1983, p. 232. https://ir.cwi.nl/pub/13008
• T. Parthasarathy and T. E. S. Raghavan, An order field property for stochastic games when one player controls the transition probabilities, Game Theory Conference, Cornell, 1978; cited in Kallenberg 1983, p. 233. https://ir.cwi.nl/pub/13008

Why optimize only transient policies?

A Markov decision model describes a system that repeatedly occupies a state, receives a reward when an action is chosen, and then moves according to action-dependent probabilities. Termination may occur after any action. In a model with signed rewards, a policy that continues indefinitely can have a different total-reward behavior from one that eventually leaves the active states. Section 3.3 of Kallenberg's 1983 monograph therefore asks for the best policy within the transient class. The restriction occurs naturally in stopping problems: a decision maker may continue for a while, but the expected number of visits to each active state must remain finite.

The chapter relates that policy problem to a finite linear program. The central question is stronger than finding a policy with a large average over initial states. It asks for one policy that is optimal from every initial state among all transient policies, including policies that randomize and use the entire observed history. Kallenberg's Theorem 3.3.5 says that an extreme optimal point of the program identifies such a policy, and that the policy can be pure and stationary. Theorem 3.3.5, p. 57.

The finite model and its policies

Let $E=\{1,\ldots,N\}$ be a nonempty finite state set. Each state $i$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is selected, the system earns the real reward $r_{ia}$ and then moves to $j$ with probability $p_{iaj}\ge0$. The row sum $\sum_jp_{iaj}$ is at most one; any missing mass represents termination. Action sets can differ across states. These are the conventions of Section 2.2, pp. 19–20.

A policy $R$ selects an action distribution at each decision epoch. It may depend on the entire state-action history. A Markov policy depends only on time and the current state; a stationary policy uses the same state-dependent distribution at every time; a pure stationary policy selects one action $f(i)\in A(i)$ in each state. These four classes are denoted $C$, $C_M$, $C_S$, and $C_D$. The first decision occurs at time $t=1$ in the book.

Write $\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ for the chance of being in state $j$ and choosing action $a$ at time $t$, given initial state $i$. A policy is transient if the expected number of visits to each state is finite from every initial state:

$$\sum_{t=1}^{\infty}\mathbb P_R(X_t=j\mid X_1=i)<\infty\qquad(i,j\in E).$$

For such a policy, its expected total reward $v_i(R)$ is finite. Section 3.3 assumes that at least one transient policy exists. Its transient value is $w_i=\sup\{v_i(R):R\text{ transient}\}$, which can still be infinite as the policy varies. Section 2.2, pp. 21–23; §3.3, pp. 49–50.

Formalization targets

Fix positive weights $\beta_j>0$. The linear program (3.3.7) maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative state-action arrays satisfying the flow equations

$$\sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}=\beta_j\qquad(j\in E).$$

Its feasible set is $P$. A transient stationary rule $\pi$ has an occupation vector $x(\pi)$, where $x_{ia}$ is the $\beta$-weighted expected number of visits to state-action pair $(i,a)$. Theorem 3.3.3 identifies transient stationary rules bijectively with $P$ and identifies extreme points with pure rules. Theorem 3.3.4 compares the occupation sets of all four policy classes: $\overline{K(D)}\subset K(S)=K(M)=K=P$, where the bar means closed convex hull. Theorems 3.3.3–3.3.4, pp. 54–55.

The goal is Theorem 3.3.5, p. 57. If $x^*$ is an extreme optimal solution of that program and $f_*(i)$ is the action with $x^*_{i f_*(i)}>0$, then the pure stationary policy $f_*^\infty$ is transient and

$$v_i(R)\le v_i(f_*^\infty) \qquad\text{for every transient policy }R\text{ and every }i\in E.$$

A stronger companion statement is Theorem 3.3.6, p. 58: under the correspondence of Theorem 3.3.3, a stationary policy is optimal transient exactly when its occupation vector is optimal for (3.3.7), in the two directions printed on the page. The milestone list follows the chapter's numbered results on the finite-value Bellman equation, the smallest superharmonic vector, the stationary-policy/LP correspondence, the four occupation sets, and the preservation of optimality. The goal itself does not assume that $w$ is finite; the existence of an extreme LP optimum is its stated premise.

What the result gives

An LP optimum is a vector of occupation amounts, not an implementable policy by itself. Theorem 3.3.5 converts an extreme optimum into an action choice at each state. It also upgrades a scalar objective weighted by $\beta$ to simultaneous optimality of the resulting policy from every initial state. This is the bridge between the finite optimization problem and the original control problem. The scope is specifically transient optimality: Example 3.3.4, p. 58 gives a policy outside that comparison class with larger total reward.

The result is proved in the book. The work here is to give its model, occupation map, linear program, and numbered supporting statements precise Lean interfaces that can later receive machine-checked proofs. The reusable parts include finite substochastic MDP data, history-dependent policy semantics, transient visit sums, and state-action occupation vectors. The theorem proofs are open in this proposal.

Where the difficulty lies

Optimizing a weighted sum of rewards is not, by itself, the same as optimizing every state's reward. The linear program also describes flows of expected visits, while the theorem talks about actual policies and all initial states. A solver must account for both links without assuming that all policies are stationary. The geometry of an extreme feasible point matters because the theorem selects an action from each state using a positive coordinate. Existence of a transient policy does not by itself bound the supremum of transient rewards; Example 3.3.1, p. 50 makes that distinction explicit.

Formalization scope

Lean uses Fin N with $N>0$ for states and a finite action type with a state-dependent finite nonempty available-action set. Only available state-action pairs index occupation vectors and LP variables. Transition rows are substochastic, not necessarily stochastic. Rewards are real and may have either sign. A general policy is a normalized action kernel on full finite histories; its Markov, stationary, and pure stationary subclasses remain distinct. The history list is stored newest first, and Lean's time index zero corresponds to the book's time one. All state-action probabilities are finite sums over histories; transience is summability of state-visit probabilities, and occupation counts are infinite sums used under that condition.

The LP flow constraints are equalities and $\beta$ is strictly positive. The goal does not normalize $\beta$ to a probability distribution, matching (3.3.7); Theorem 3.3.4 uses the initial-distribution convention of p. 55 and hence normalizes it. Theorem 3.3.3 uses the matrix inverse $(I-P(\pi))^{-1}$ only for transient stationary rules. For Theorems 3.3.1–3.3.2, nonemptiness of the transient class and boundedness above of each transient reward set make the real supremum meaningful. Theorem 3.3.5 uses neither boundedness as an extra hypothesis nor a restriction of the comparison class to stationary policies. A formalization that compares $f_*^\infty$ only with stationary (or Markov) policies, or that identifies the classes $C$, $C_M$, $C_S$, $C_D$, would make Theorems 3.3.4 and 3.3.5 much weaker or trivial, and is ruled out: the comparison class is every history-dependent randomized transient policy. Mathlib's finite sums, matrices, summability, convex hull, and extreme-point definitions provide the general library interface. Contributions establishing the policy/occupation identities and the chapter's numbered milestones are within scope.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, §§2.2 and 3.3, pp. 19–23 and 49–60. Publisher repository.

Motivation

Integer linear programming asks for the best point whose coordinates are integers, even though linear programming methods naturally search over real points. In his 1958 note, Gomory describes a systematic way to add a constraint that excludes a fractional simplex solution while retaining every nonnegative integer solution. This mission isolates that single cut and its effect on the objective value. The note announces an iterative finite algorithm, but explicitly defers a proof of finiteness to another treatment. The target here is the cut's correctness for one tableau.

The cut belongs to the history of cutting plane methods for integer programs. Related formalized objects include a Chvátal closure and intersection cuts based on lattice free sets, but their data and cut constructions differ from the row and fractional part formula in Gomory's note. The note itself contrasts its systematic row operation with earlier problem specific constraints used by Dantzig, Fulkerson, and Johnson and by Markowitz and Manne. Those comparisons explain why a reusable row formula is useful; they do not assert an identity between the different cuts.

Setting

A tableau is a finite array of real numbers $a'_{i,j}$. Row $0$ represents the objective variable $w$; rows $1,\ldots,m$ represent $x'_1,\ldots,x'_m$. Column $0$ holds constants; columns $1,\ldots,n$ multiply the negatives of the variables $t'_1,\ldots,t'_n$. A solution of (2) is a pair $(x',t')$ satisfying

$$x'_i=a'_{i,0}+\sum_{j=1}^{n}a'_{i,j}(-t'_j),\qquad 0\le i\le m.$$

The original integer program requires $w=x'_0$, every $x'_i$, and every $t'_j$ to be nonnegative integers. The simplex solution of this tableau has $t'=0$ and $x'_i=a'_{i,0}$. It is a real tableau solution, whether or not any of its coordinates are integers.

Choose a row $i_0$ whose constant $a'_{i_0,0}$ is not an integer. For each coefficient let $n'_{i_0,j}=\lfloor a'_{i_0,j}\rfloor$ be the greatest integer at most that coefficient, and let $f'_{i_0,j}=a'_{i_0,j}-n'_{i_0,j}$ be its fractional part. Equation (3) defines a new variable

$$s_1=-f'_{i_0,0}-\sum_{j=1}^{n}f'_{i_0,j}(-t'_j).$$

The augmented system (2)* adds this equation to the tableau. Feasibility now also requires $s_1\ge0$; an integer solution additionally requires $s_1\in\mathbb Z$. For example, the one row relation $x'=\tfrac12-\tfrac12t'$ admits the integer solution $(x',t')=(0,1)$, and its cut value is $s_1=0$. At the simplex point $t'=0$, the same cut value is $-\tfrac12$.

Formalization targets

Fractional cut and integer optimum

The main target combines exclusion of the simplex solution, exact correspondence of nonnegative integer solutions, and equality of their attained objective values. Writing $\mathcal I_2$ and $\mathcal I_{2^*}$ for the two sets of nonnegative integer solutions, the correspondence is

$$(x',t')\in\mathcal I_2\quad\Longleftrightarrow\quad (x',t',s_1(x',t'))\in\mathcal I_{2^*}.$$

Every member of $\mathcal I_{2^*}$ has the displayed cut value for $s_1$, and the projection that drops $s_1$ leaves $w$ unchanged. Consequently a real $W$ is the greatest attained $w$ value for (2) exactly when it is the greatest attained value for (2*). The statement does not assume either set has a maximum.

Supporting claims

The milestones follow the paragraphs on page 277: projection of feasible solutions, the impossibility of integer solutions when the selected row has a fractional constant but only integral other coefficients, exclusion of the simplex point, the identity proving $s_1$ integral, and its nonnegativity on integer solutions. These are the claims the note uses to pass from the cut formula to the correspondence and the objective statement.

Significance

The result certifies that equation (3) removes the current fractional simplex point while retaining every integer candidate and its objective value. It is the local correctness condition needed before one can safely reoptimize an integer program after adding this constraint. The note's argument is a mathematical result about one tableau, independent of whether the subsequent sequence of pivots terminates.

This mission supplies a machine checkable interface for the tableau, the fractional cut, and the projection between their integer feasible sets. The theorem statements are drafted and compile with open proofs; this mission does not claim that the paper's result already has a machine checked proof here. A completed proof would make the one cut result available for later developments about iterations, optimization, or stronger cut families.

Difficulty

The cut value is visibly at least $-f'_{i_0,0}$ when the nonbasic variables are nonnegative, but that inequality alone does not give $s_1\ge0$: the right side is negative for the chosen row. The key additional statement is that the real expression for $s_1$ is an integer on an integer tableau solution. Formalization must preserve both facts while using the same sign convention for the tableau and the cut. Merely defining the augmented solution as a pair together with its computed cut value would make the correspondence automatic and would omit the new variable's integrality and nonnegativity requirements.

Formalization scope

Lean uses real valued tableau coefficients and real valued variables with a separate predicate for being an integer. This lets the fractional simplex point and integer feasible points inhabit the same space. The row and column sets are finite, including the cases $m=0$ and $n=0$; row $0$ is $w$, column $0$ is the constant column, and Lean's Fin n index $j$ denotes the paper's $t'_{j+1}$. The selected row can be row $0$ in Lean. Gomory chooses a constraint row, but the local cut argument needs only the selected row's variable to be integral, and $w$ is integral in the stated problem. Every variable, including $w$ and the added $s_1$, is required to be nonnegative and integral in an integer solution.

The fractional part uses the greatest integer at most a real number, including negative coefficients. The objective comparison uses greatest elements of the sets of attained $w$ values, so empty and unbounded sets receive no artificial supremum. Nonnegative constants and objective row coefficients are features of the simplex setting, but the five local claims and goal remain valid without those extra hypotheses. The paper's loose phrases “cuts off,” “one-one correspondence,” and “can be replaced” are represented by infeasibility of the augmented simplex point, a unique extension and projection preserving $w$, and equivalence of greatest attained $w$ values, respectively.

The mission does not formalize the derivation of (2) from (1) by simplex pivots, dual simplex reoptimization, finiteness of repeated cutting, the $m+n+2$ equation bound and deletion of re-entering $s$ variables, the suggested choice of largest fractional part, or the reported E101 runs. These concern an iterative process the note does not define fully, or empirical observations. Reusable contributions include a verified fractional part identity, the integer extension theorem, and solution set correspondence for a real tableau.

Selected references

• Ralph E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the American Mathematical Society 64(5), 1958, 275–278. DOI: 10.1090/S0002-9904-1958-10224-4.
• George B. Dantzig, R. Fulkerson, and S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 1954, 393–410. DOI: 10.1287/opre.2.4.393.

Motivation

Nonlinear conjugate gradient methods minimize a smooth function $f$ of $n$ variables using only function values, gradients and a few vectors of storage. They are the method of choice when $n$ is so large that quasi-Newton matrices cannot be stored, and they remain a standard component of large-scale optimization software. Their convergence theory is delicate: the classical results assume exact line searches, while practical codes accept any steplength satisfying inexpensive inexact conditions.

Gilbert and Nocedal (INRIA RR-1268, 1990; journal version SIAM J. Optim. 2 (1992)) organized the global convergence theory of these methods around a single device and proved two families of results. This mission covers the first: every conjugate gradient method whose parameter $\beta_k$ is bounded in absolute value by the Fletcher–Reeves value converges under the strong Wolfe line search.

Timeline. Fletcher and Reeves (1964) and Polak and Ribière (1969) introduced the two best-known choices of $\beta_k$. Zoutendijk (1970) and Wolfe (1969, 1971) established the summability condition now called Zoutendijk's condition. Al-Baali (1985) proved that the Fletcher–Reeves method with the strong Wolfe line search and $\sigma_2 < \tfrac12$ generates descent directions and satisfies $\liminf\|g_k\| = 0$. Touati-Ahmed and Storey (1990) treated nonnegative hybrids. Gilbert and Nocedal (1990) extended Al-Baali's theorem to every $\beta_k$ with $|\beta_k| \le \beta_k^{FR}$, which admits negative values and yields a convergent modification of the Polak–Ribière method.

Setting

Let $E$ be a finite-dimensional real inner product space and $f : E \to \mathbb R$ continuously differentiable, with gradient $g = \nabla f$ for that inner product. Starting from $x_1$, the method generates

$$d_1 = -g_1,\qquad d_k = -g_k + \beta_k d_{k-1}\ (k\ge 2),\qquad x_{k+1} = x_k + \alpha_k d_k,$$

where $g_k = g(x_k)$, $\beta_k$ is a scalar and $\alpha_k > 0$ a steplength found by a one-dimensional search. The Fletcher–Reeves and Polak–Ribière scalars are

$$\beta_k^{FR} = \frac{\|g_k\|^2}{\|g_{k-1}\|^2},\qquad \beta_k^{PR} = \frac{\langle g_k, g_k - g_{k-1}\rangle}{\|g_{k-1}\|^2}.$$

Assumptions 2.1: the level set $\mathcal L = \{x : f(x) \le f(x_1)\}$ is bounded, and on an open neighbourhood $\mathcal N$ of $\mathcal L$ the gradient is Lipschitz: $\|g(x) - g(\tilde x)\| \le L\|x - \tilde x\|$.

A steplength satisfies the Wolfe conditions with $0 < \sigma_1 < \sigma_2 < 1$ if

$$f(x_k + \alpha_k d_k) \le f(x_k) + \sigma_1\alpha_k\langle g_k, d_k\rangle,\qquad \langle g(x_k+\alpha_k d_k), d_k\rangle \ge \sigma_2\langle g_k, d_k\rangle,$$

and the strong Wolfe conditions if the second inequality is replaced by $|\langle g(x_k+\alpha_k d_k), d_k\rangle| \le -\sigma_2\langle g_k, d_k\rangle$. The angle $\theta_k$ between $-g_k$ and $d_k$ is given by $\cos\theta_k = -\langle g_k, d_k\rangle/(\|g_k\|\|d_k\|)$, and the Zoutendijk condition is $\sum_{k\ge1}\cos^2\theta_k\|g_k\|^2 < \infty$.

Formalization targets

Goal: Theorem 3.2

Under Assumptions 2.1, for any method of the above form with

$$|\beta_k| \le \beta_k^{FR}\quad (k \ge 2)$$

and steplengths satisfying the strong Wolfe conditions with $0 < \sigma_1 < \sigma_2 < \tfrac12$,

$$\liminf_{k\to\infty}\|g_k\| = 0 .$$

The sequence $\beta_k$ is arbitrary within the bound; the statement contains no constants.

Milestones

• Theorem 2.1 (i) (Zoutendijk): for any iteration $x_{k+1} = x_k + \alpha_k d_k$ with descent directions and Wolfe steps, $\sum_{k\ge1}\cos^2\theta_k\|g_k\|^2 < \infty$.
• Lemma 3.1: under $|\beta_k| \le \beta_k^{FR}$ and the strong Wolfe curvature condition with $\sigma_2 < \tfrac12$, every $d_k$ is a descent direction and

$$-\sum_{j=0}^{k-1}\sigma_2^j \le \frac{\langle g_k, d_k\rangle}{\|g_k\|^2} \le -2 + \sum_{j=0}^{k-1}\sigma_2^j .$$

• (3.5): there are $c_1, c_2 > 0$ with $c_1\|g_k\|/\|d_k\| \le \cos\theta_k \le c_2\|g_k\|/\|d_k\|$.

Further statements

Theorem 2.1 (ii) (the same conclusion for an ideal line search that does no worse than the first stationary point along $d_k$) and the convergence of the hybrid method (3.7), $\beta_k = \max(-\beta_k^{FR}, \min(\beta_k^{PR}, \beta_k^{FR}))$.

Significance

Theorem 3.2 shows that descent and global convergence of Fletcher–Reeves-type methods do not depend on the exact formula for $\beta_k$, only on the bound $|\beta_k| \le \beta_k^{FR}$. Its main consequence is the hybrid method (3.7), which keeps the Polak–Ribière choice whenever it lies in $[-\beta_k^{FR}, \beta_k^{FR}]$, and so retains the practical efficiency of Polak–Ribière while inheriting the convergence guarantee of Fletcher–Reeves. Lemma 3.1 also shows that, under these conditions, descent need not be enforced by the line search.

The results are proved in the paper. To our knowledge none of them, nor Zoutendijk's theorem for general iterations, has a machine-checked proof in Lean; Mathlib has no theory of line search methods. A formalization would provide a reusable Zoutendijk theorem for any descent method with Wolfe steps, and a verified convergence statement for the conjugate gradient methods used in practice.

Difficulty

The obvious route to convergence of a descent method is to show $\cos\theta_k$ bounded away from zero and apply Zoutendijk's condition. For conjugate gradient methods this fails: $d_k$ accumulates previous directions and $\cos\theta_k$ can tend to zero. The argument must instead control the growth of $\|d_k\|$, which requires bounding $\langle g_k, d_{k-1}\rangle$ through the line search, and this in turn requires knowing that every $d_k$ is a descent direction with $\langle g_k, d_k\rangle$ comparable to $\|g_k\|^2$. The threshold $\sigma_2 < \tfrac12$ is exactly what keeps the geometric series in these bounds below $2$; the result fails without it.

Formalization scope

All items live in the namespace NonlinCG.FRBound. The space is a finite-dimensional real inner product space E (the paper uses "the scalar product used to compute the gradient"), and gradient f is the gradient for that product. Conventions committed to:

• Indexing follows the paper: sequences ℕ → E, used from index 1; index 0 is never constrained.
• Smoothness: every statement assumes $f$ globally $C^1$, from (1.1) "f is smooth", in addition to Assumptions 2.1 (bounded level set; $C^1$ and Lipschitz gradient on an open neighbourhood $\mathcal N$ of $\mathcal L$, with $L > 0$).
• Steplengths are positive, as in the paper's line searches.
• $\beta_k$ is a free sequence constrained by $|\beta_k| \le \beta_k^{FR}$, not the Fletcher–Reeves formula. Fixing $\beta_k = \beta_k^{FR}$ would state Al-Baali's theorem instead.
• Division: $\beta^{FR}$, $\beta^{PR}$, $\cos\theta_k$ are Lean divisions (value 0 on a zero denominator). Theorem 3.2 does not assume $g_k \ne 0$; Lemma 3.1 and (3.5) assume it, since the paper divides by $\|g_k\|^2$ there and descent is impossible at $g_k = 0$.
• Zoutendijk's sum is the summability of $\langle g_k, d_k\rangle^2/\|d_k\|^2$, which equals $\cos^2\theta_k\|g_k\|^2$ under descent.
• liminf is stated as: for every $\varepsilon > 0$ and $K$ there is $k \ge K$ with $\|g_k\| < \varepsilon$.
• (3.5) asserts existence of the constants only, as the paper does.

The goal does not assume Zoutendijk's condition or descent: both are consequences (Theorem 2.1 and Lemma 3.1) and assuming either would remove part of the theorem's content. The hypotheses are jointly satisfiable (for $f(x) = x^2/2$ on $\mathbb R$, $x_1 = 1$, $\beta_k = 0$, $\alpha_k = 0.9$, $\sigma_1 = 0.1$, $\sigma_2 = 0.25$), so the goal is not vacuous.

Needed infrastructure: line-search conditions, the descent lemma for functions with Lipschitz gradient on a set, and summability arguments for $\sum\|d_k\|^{-2}$. Zoutendijk's theorem is reusable for any descent method. Proofs of any item, and alternative arguments, are welcome.

Selected references

• J. C. Gilbert, J. Nocedal, Global convergence properties of conjugate gradient methods for optimization, INRIA Rapport de Recherche 1268, 1990. https://hal.inria.fr/inria-00075291 ; SIAM J. Optim. 2(1) (1992) 21–42, https://doi.org/10.1137/0802003
• M. Al-Baali, Descent property and global convergence of the Fletcher–Reeves method with inexact line search, IMA J. Numer. Anal. 5 (1985) 121–124. https://doi.org/10.1093/imanum/5.1.121
• R. Fletcher, C. M. Reeves, Function minimization by conjugate gradients, Comput. J. 7 (1964) 149–154. https://doi.org/10.1093/comjnl/7.2.149
• P. Wolfe, Convergence conditions for ascent methods, SIAM Rev. 11 (1969) 226–235. https://doi.org/10.1137/1011036
• D. Touati-Ahmed, C. Storey, Efficient hybrid conjugate gradient techniques, J. Optim. Theory Appl. 64 (1990) 379–397. https://doi.org/10.1007/BF00939455

Motivation

Finite Markov decision models are often described by policies that choose an action from the current state. The admissible class in a total reward problem is wider: a randomized decision may use the complete history of observed states and chosen actions. For an undiscounted infinite horizon, the expected number of visits to a state may be infinite, and the total reward may be an extended real number. It matters whether a test carried out on finitely many pure stationary policies really controls this wider class. Kallenberg's Section 3.2 answers that question for finite models whose transition rows may lose probability mass when the process terminates.

The chapter is part of a 1983 account of linear programming methods for finite Markovian control. Its Theorem 3.2.4 collects earlier characterizations of transience and relates them to a finite linear program. The historical attribution in Kallenberg's Remark 3.2.2 is precise: Veinott (1969) established the equivalence of the first three conditions for nonrandomized policies, Hordijk (1976, course notes) extended the first four to general policies, and Denardo and Rothblum (1979) established the link between pure stationary transience and the LP condition. The mission targets Kallenberg's combined five-way statement, rather than treating those partial precedents as separate conclusions. Kallenberg, pp. 42–43.

Setting

Let $E$ be a finite nonempty state space of size $N$. For every state $i$, let $A(i)$ be a nonempty finite set of actions. Choosing $a\in A(i)$ gives the transition number $p_{iaj}\ge0$ to state $j$, with $\sum_jp_{iaj}\le1$. The missing mass is the probability that the system terminates before another decision epoch. This is a substochastic model; replacing the inequality by equality would change the question. Kallenberg, §2.2.

A policy $R$ specifies, at each epoch $t\ge1$, a probability distribution on $A(i_t)$ after the full history $(i_1,a_1,\ldots,a_{t-1},i_t)$. It may be randomized and may depend on all preceding states and actions. A memoryless policy depends only on the epoch and current state. A pure stationary policy $f^\infty$ chooses a single admissible action $f(i)$ in state $i$ at every epoch. Write $P_R(X_t=j\mid X_1=i)$ for the probability of state $j$ at epoch $t$ from initial state $i$. The policy is transient when $\sum_{t\ge1}P_R(X_t=j\mid X_1=i)<\infty$ for every pair $i,j$. Kallenberg, pp. 20–23.

The finite-horizon survival recursion starts from $y_i^0=1$ and sets $y_i^t=\max_{a\in A(i)}\sum_jp_{iaj}y_j^{t-1}$ for $t\ge1$. A model is contracting if there is a strictly positive vector $\mu$ and a scalar $0\le c<1$ for which $\sum_jp_{iaj}\mu_j\le c\mu_i$ for every admissible $(i,a)$. These objects are determined by the transition system; rewards do not enter the five-way characterization. Kallenberg, p. 23 and pp. 41–43.

Formalization targets

Five equivalent conditions

For any fixed $\beta_j>0$, Theorem 3.2.4 states the equivalence of: transience of every pure stationary policy; transience of every policy; $\max_i y_i^N<1$; contraction; and existence of a finite solution of

$$\max\left\{\sum_{i\in E}\sum_{a\in A(i)}x_{ia}:\ \sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}\le\beta_j\ (j\in E),\quad x_{ia}\ge0\right\}.$$

“Finite solution” means an attained finite optimum. The $\beta_j$ are arbitrary positive right-hand sides, not a choice that the theorem is allowed to make after seeing the model. The state count $N$ is the exponent in $y^N$, and the inequality is strict. Kallenberg, Theorem 3.2.4, pp. 42–43.

Supporting targets

The milestones follow the results the chapter uses on the way to Theorem 3.2.4, in attack order:

1. Theorem 2.5.1 (Derman–Strauch) and its Corollary 2.5.1: for a fixed initial distribution, a memoryless policy reproduces the state-action probabilities $P_R(X_t=j,Y_t=a\mid X_1=i)$ of any policy or of any countable mixture of policies.
2. Lemma 3.2.1: under Assumption 3.2.1, $\lim_{\alpha\uparrow1}v_i^\alpha(R)=v_i(R)$ in $[-\infty,+\infty]$.
3. Theorem 3.2.1: under Assumption 3.2.1 there is a pure stationary policy $f^\infty$ with $v(f^\infty)=v$, where $v_i=\sup_Rv_i(R)$.
4. Theorem 3.2.2: if $v$ is p-summable, then $v_i=\max_{a\in A(i)}\{r_{ia}+\sum_jp_{iaj}v_j\}$.
5. Theorem 3.2.3: if some policy is transient, some pure stationary policy is transient.
6. Lemma 3.2.2: $y_i^t=\sup_R\sum_jP_R(X_{t+1}=j\mid X_1=i)$, attained by the policy $(f_t,f_{t-1},\dots,f_1,f_1,\dots)$ built from maximizers of the recursion.

Assumption 3.2.1 says that every policy's expected total reward $v_i(R)=\lim_T\sum_{t\le T}v^t_i(R)$ exists in $[-\infty,+\infty]$; it is a hypothesis of items 2–4 only. Kallenberg, pp. 32–33, 37–42.

Significance

The theorem gives four finite or structured ways to recognize a property quantified over all policies. The survival condition uses only $N$ recursion steps, and the contraction condition supplies a weighted geometric bound on continuation. The LP links the same property to a finite-dimensional optimization problem. Each characterization can serve a different later argument without assuming the policy class has been reduced to stationary rules. Kallenberg, Theorem 3.2.4.

The five-way theorem and its supporting results are proved in the book; this mission asks for machine-checked proofs of their stated finite-model versions. The Derman–Strauch policy result is quoted by Kallenberg without proof, so its formal proof is a separate substantial contribution. None of these results has a machine-checked proof yet. The general history and occupancy definitions can be reused by later total-reward and constrained-control missions.

Difficulty

Checking only the finitely many pure stationary transition matrices does not directly bound the occupation counts of a history-dependent policy. Such a policy can change its action distribution after each observed path, and it need not be a mixture of stationary policies chosen once at the start. Likewise, $y_i^N<1$ is a finite-horizon bound, whereas transience is a statement about an infinite series of visit probabilities. The main difficulty is connecting these different quantifiers without changing the policy class. The LP condition adds a second boundary: its constraints use $\le\beta_j$, and finite value includes attainment. Kallenberg, pp. 41–45.

Formalization scope

States are Fin N with $N>0$, and actions form one finite ambient type with a nonempty admissible subset $A(i)$ at each state. Transitions are real nonnegative numbers with row sums at most one. Epoch $t=1$ is Lean index zero. A history records states and earlier actions; policy decision rules are normalized and supported on the current state's admissible actions. Occupancies are finite sums of transition products, so the definition of transience is summability of a nonnegative real sequence, not a bound on an individual term.

The reward layer is separate from the transition system. It uses extended real limits under Assumption 3.2.1, while the five-way goal needs no reward hypothesis. Sums $\sum_jp_{iaj}x_j$ of extended reals are only asserted for p-summable $x$, where no $+\infty$ and $-\infty$ meet with positive coefficients; the convention $0\cdot(\pm\infty)=0$ is the book's. The LP objective and constraints range only over admissible state-action pairs. Its finite-solution predicate includes a feasible optimizer. Contraction allows an arbitrary componentwise positive weight $\mu$ and requires $0\le c<1$; it does not normalize $\mu$ to the all-ones vector. The $N$-step test uses the cardinality of the original state space.

All-policy transience means every history-dependent randomized policy. Restricting that quantifier to Markov or stationary policies would remove the central content of the theorem. Useful contributions include finite-history probability identities, the Derman–Strauch occupancy theorem, the maximal-survival recursion, the stationary total-optimality result, and the finite LP characterization. The occupancy and policy definitions are reusable beyond this mission.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• C. Derman and R. E. Strauch, A note on memoryless rules for controlling sequential control processes, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699618
• A. F. Veinott Jr., Discrete dynamic programming with sensitive discount optimality criteria, Annals of Mathematical Statistics 40 (1969), 1635–1660. https://doi.org/10.1214/aoms/1177697379
• E. V. Denardo and U. G. Rothblum, Optimal stopping, exponential utility, and linear programming, Mathematical Programming 16 (1979), 228–244. https://doi.org/10.1007/BF01582110
• A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25 (1979), 352–362. https://doi.org/10.1287/mnsc.25.4.352

Motivation

Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).

The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).

Setting

Let $E$ be a nonempty finite set of states. Each $i\in E$ has a nonempty finite action set $A(i)$. Taking $a\in A(i)$ earns a real reward $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$. A row may sum to less than one; the missing probability is termination. A policy $R$ specifies a probability distribution over $A(i)$ after every finite history ending in $i$. A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action $f(i)$ in each state. These are the classes $C$, $C_M$, $C_S$, and $C_D$ of §2.2 (Kallenberg 1983, pp. 19–21).

The standing contraction assumption supplies weights $\mu_i>0$ and $0\le\alpha<1$ with

$$\sum_{j\in E}p_{iaj}\mu_j\le\alpha\mu_i \qquad(i\in E,\ a\in A(i)).$$

It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).

For an initial probability distribution $\beta$, with $\beta_i\ge0$ and $\sum_i\beta_i=1$, write $x_{ja}(R)$ for the expected total number of visits to state $j$ at which action $a$ is chosen, averaged over the initial state. Let $K$, $K(M)$, $K(S)$, and $K(D)$ collect these frequency vectors for the four policy classes. The frequency polytope $P$ consists of nonnegative vectors $x$ satisfying conservation of expected flow at each state:

$$\sum_{a\in A(j)}x_{ja} -\sum_{i\in E}\sum_{a\in A(i)}p_{iaj}x_{ia}=\beta_j \qquad(j\in E).$$

These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).

Formalization targets

The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every $\beta_i>0$, and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).

The mission goal allows zero entries in the initial distribution and compares all four policy classes:

$$\overline{K(D)}=K(S)=K(M)=K=P.$$

The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, $K(D)$ is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).

Significance

The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over $P$ without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).

The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.

Difficulty

For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of $K$ with $P$ therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When $\beta_j=0$, different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).

Formalization scope

States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index $n=0$ represents the book's period $t=1$. The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.

The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository copy.

Why multi-level programs are hard

Multi-level programs model a hierarchy of decision makers: a leader commits to a decision, a follower optimises given it, a follower of the follower optimises given both, and so on. Bilevel programs are the standard model of Stackelberg competition, toll setting, network interdiction and many other leader–follower problems in operations research (Candler and Townsley 1982; Bard and Falk 1982). When every level has a linear criterion and the constraints are linear, each player's problem looks like a linear program, and it is natural to hope that the whole hierarchy is solvable in polynomial time.

R. G. Jeroslow's 1985 paper (Math. Programming 32, 146–164) shows that this hope fails at every level of the polynomial hierarchy: a $(p+1)$-level linear program with fixed criteria can encode the truth of a $\Sigma_p$ quantified Boolean sentence. The result places multi-level linear programming in the polynomial hierarchy and is widely cited for the $\Sigma_p$-hardness of such programs; NP-hardness of bilevel linear programs (Corollary 4.6) is its special case $p=1$.

Setting

A multi-level program has real variables $x=(x^1,\dots,x^p)$, a feasible set $S_0$ (a polyhedron $\{x: \sum_i A^ix^i\ge b\}$ in the linear case), and players $p,p-1,\dots,1$ who move in that order; player $i$ controls $x^i$ and minimises a fixed linear criterion $c^ix$. The solution sets are defined from the last mover upwards: $S_1$ is the set of $x\in S_0$ at which player 1's criterion is minimal given the choices of all earlier movers, and in general $S_{j}$ keeps the points of $S_{j-1}$ minimising $c^jx$ among the points of $S_{j-1}$ that agree with $x$ on $x^{j+1},\dots,x^p$. The value is $c^px$ on $S_p$, when $S_p\neq\emptyset$. The sets $S_j$ can be empty even when $S_0$ is a nonempty polytope: the paper's four-level Example has $S_4=\emptyset$ because $S_3$ is not closed.

A propositional formula $F$ over blocks of atoms $X_1,\dots,X_p$ (block $X_k$ has $n_k$ atoms) is encoded by the linear system $L_F$: one variable $x(G)\in[0,1]$ per non-atomic subformula, with the inequalities (3.1a)–(3.1c) for $\vee$, $\wedge$, $\neg$. The quantifier of block $X_k$ is $Q_k=\exists$ when $p-k$ is even, so

$$(\exists X_p)(\forall X_{p-1})\cdots(Q_1X_1)\,[F(X_1,\dots,X_p)=1] \qquad (3.3)$$

is a $\Sigma_p$ sentence.

The game $J'(F)$ adds a bookkeeper, player $0$, who moves last. Player $k\ge1$ controls the atoms of $X_k$, and player $1$ also controls auxiliary variables $y$; the bookkeeper controls the $x(G)$, a variable $u$ fixed to $1$, and auxiliary variables $z$. Two gadgets, (4.1) and (4.6), let the bookkeeper and player 1 turn the linear criteria into the piecewise-linear functions $Z_k=1-x(F)+2\sum_jP(x_{kj})$ (or $x(F)+\dots$ for universal $Q_k$) and $Z_1=(1-x(F))+fr(1-x(F))+10L\sum_j fr(x_{1j})+\dots$, where $L$ is the length of $F$, $fr(x)=\min\{x,1-x\}$, and $P(x)=1$ at $x\in\{0,1\}$, $2$ otherwise.

Formalization targets

Goal: Theorem 4.5 ($p\ge2$)

Let $S$ be the set of optimal solutions $S_{p+1}$ of $J'(F)$. Then $S\neq\emptyset$; at every optimum all atom variables and all $x(G)$ are binary; and

$$x(F)=1 \iff (3.3)\ \text{holds},\qquad \text{value}(J'(F)) = 2n_p+1-x(F).$$

Moreover, when (3.3) holds, $v\in\mathbb R^{n_p}$ is player $p$'s block in some optimum iff $v$ is binary and the $\Pi_{p-1}$ sentence (4.17) holds at the truth valuation of $v$.

Milestones

In attack order: Lemma 3.1 (correctness of $L_F$ on binary inputs); Lemma 4.1 (robustness of $L_F$ near binary inputs); Lemmas 4.2 and 4.3 (the bottom two levels of a bounded linear multi-level program are solvable, via LP duality); the bookkeeper identities $z=|2y-x|$ and $z=fr(x)$ in $S_1$; (4.2) and (4.3) (player 1's and player $k$'s responses on the gadgets); Lemma 4.4 (the induction on $k$ with the higher blocks fixed). Companion theorems: Corollary 4.6 (the bilevel case: value $0$ iff $(\exists X_1)F$), the §2 Example, and Proposition 3.2 (the pure binary game $J(F)$).

Significance

The theorem shows that deciding the value of a $(p+1)$-level linear program with fixed criteria is at least as hard as deciding $\Sigma_p$ sentences, so known exact algorithms for multi-level linear programs cannot be expected to run in polynomial time once $p\ge2$, and even recognising an optimal move is $\Pi_{p-1}$-hard. The bilevel case is an early NP-hardness proof for bilevel linear programming, and the construction (a bookkeeper player and absolute-value gadgets that force binary choices) is a template for hardness reductions to leader–follower problems.

The result is proved in the paper but, to our knowledge, has no machine-checked formalization. A formal development makes precise the solution concept (conditional rather than lexicographic minimisation), which the literature states in several inequivalent ways, and checks a proof whose printed version leaves cases to the reader (the $\wedge$, $\neg$ cases of Lemma 4.1, the universal cases of Lemma 4.4) and applies Lemma 4.3 to a feasible set that is unbounded (the (4.1) variable $z$ has no upper bound).

Difficulty

The obvious argument, "each existential player picks a satisfying assignment and each universal player a counterexample", works for the pure binary game $J(F)$ (Proposition 3.2) but not for continuous variables: a player may choose fractional values, and the solution sets of a multi-level program need not exist (the §2 Example). The work is in showing that every player is forced to binary choices. Player 1's fractional choices are ruled out only through the robustness estimate of Lemma 4.1 with the weight $10L$, and the existence of optimal solutions at every level has to be established along the induction, since it fails for general three-level programs.

Formalization scope

• Players are indexed from $0$; player $i$ optimises at level $i+1$. In $J'(F)$ the players are $0,\dots,p$ as in the paper; in the §2 Example and in $J(F)$ the paper's player $i$ is index $i-1$. Blocks are 0-based: block k : Fin p is the paper's $X_{k+1}$, owned by player $k+1$ in $J'(F)$.
• solSet encodes the conditional minimisation of (3.7), p. 152. HasValue N w requires $S_N\neq\emptyset$; the value $+\infty$ is not modelled.
• Formulas use $\neg,\wedge,\vee$ (the paper rewrites $\to$ as $\neg G_1\vee G_2$); the length counts atoms and connectives. Data are real; the paper's rationality assumption plays no role in the statements.
• The bookkeeper controls the $x(G)$ and has criterion "$+z$ on (4.1) gadgets, $-z$ on (4.6) gadgets, and $+x(G)$ for each non-atomic subformula," as stated on p. 155. The (4.1) variable $z$ has no upper bound. The constant $1$ of (4.4)/(4.7) is the variable $u$ with $u=1$.
• "Binary value, zero iff $F\in B_p$" is stated exactly: the value is $2n_p+1-x(F)$, and $x(F)=1$ iff (3.3). "All optimal solutions are binary" covers the atom variables and the $x(G)$, not the gadget variable $z$, which equals $2$ at $y=1$, $\xi=0$.
• The goal is not trivialisable: its first conjunct asserts that the optimal set is nonempty, which fails for general multi-level programs (the §2 Example), so the remaining conjuncts are not vacuous.

A complete development needs a linear-programming duality argument for Lemma 4.2 (Mathlib has IsExtreme and Set.extremePoints; LP duality is on the platform as a single-level theorem) and an induction over the levels of the game. The definitions MultilevelProgram, solSet and the formula encoding LSys are reusable for other complexity results on hierarchical optimisation. Proofs of any milestone, including the generic Lemmas 4.2–4.3 and the formula Lemmas 3.1 and 4.1, are welcome independently.

Selected references

• R. G. Jeroslow, The polynomial hierarchy and a simple model for competitive analysis, Mathematical Programming 32 (1985) 146–164. https://doi.org/10.1007/BF01586088
• W. Candler and R. Townsley, A linear two-level programming problem, Computers & Operations Research 9 (1982) 59–76. https://doi.org/10.1016/0305-0548(82)90006-5
• J. F. Bard and J. E. Falk, An explicit solution to the multi-level programming problem, Computers & Operations Research 9 (1982) 77–100. https://doi.org/10.1016/0305-0548(82)90007-7
• L. J. Stockmeyer, The polynomial-time hierarchy, Theoretical Computer Science 3 (1976) 1–22. https://doi.org/10.1016/0304-3975(76)90061-X

Motivation

Reliability theory classifies life distributions by how they age. A device whose failure rate tends to increase over time is "wearing out", and the class of distributions with increasing hazard rate average (IHRA) is the one that is closed under forming coherent systems of independent components (Birnbaum, Esary and Marshall, 1966). This makes IHRA the natural ageing class for systems. It also raises a question: which physical failure mechanisms produce IHRA lives?

Esary, Marshall and Proschan's paper Shock Models and Wear Processes (Ann. Probability 1, 1973) answers this for two kinds of mechanism. In the first, damage arrives in discrete amounts at the epochs of a Poisson process of shocks. In the second, damage accumulates continuously. In both, the device fails when the accumulated damage first exceeds a fixed capacity. This mission covers the second kind: a wear process $\{Z(t), t \ge 0\}$ and its first passage time above a level. The paper shows that the first passage time is IHRA under three qualitative conditions: wear starts at zero and only grows, the process is Markov, and accumulated wear and age make further wear more likely. Nothing else is assumed about the law of the wear.

A short timeline. Birnbaum, Esary and Marshall (1966) introduced the IHRA class and proved it is closed under coherent systems. Morey (1965) studied first passage times of wear processes under an extra monotonicity assumption. Esary, Marshall and Proschan (1973), §4, proved the IHRA property first for Poisson shocks with i.i.d. damages (Corollary 4.2, (4.7)), then for dependent damages (Lemma 4.1b, (4.7b)), and finally for continuous wear (Theorem 4.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space. "Decreasing" means non-increasing throughout.

A survival function $\bar F$ is IHRA if $t \mapsto [\bar F(t)]^{1/t}$ is decreasing on $t > 0$ (p. 631). For an exponential life, $[\bar F(t)]^{1/t}$ is constant. IHRA says the average failure rate over $[0, t]$ never decreases.

Dependent damages. Let $X_1, X_2, \dots$ be nonnegative random variables, the damages caused by successive shocks, and let $Z_0 = 0$ and $Z_k = X_1 + \dots + X_k$. The paper's conditions (p. 636) are:

• (4.3) the conditional law of $X_k$ given $X_1, \dots, X_{k-1}$ depends only on $Z_{k-1}$;
• (4.4) $P\{X_k \le u \mid Z_{k-1} = z\}$ is decreasing in $z \ge 0$ (accumulated damage lowers resistance);
• (4.5) $P\{X_k \le u \mid Z_{k-1} = z\} \ge P\{X_{k+1} \le u \mid Z_k = z\}$ for $z \ge 0$ (later shocks are more severe).

Wear process. $Z(t)$ is the wear accumulated in $[0, t]$. The conditions (pp. 640–641) are:

• (4.8) $Z(0) = 0$ and $Z(t + \Delta) - Z(t) \ge 0$ for all $t, \Delta \ge 0$, with probability one;
• (4.9) $\{Z(t), t \ge 0\}$ is a Markov process;
• (4.10) $P\{Z(t + \Delta) - Z(t) \le u \mid Z(t) = z\}$ is decreasing in both $z$ and $t$ in the region $t \ge 0$, $z \ge 0$, $\Delta \ge 0$.

The first passage time above a level $x$ is $T_x = \inf\{t : Z(t) > x\}$. Its survival function is $\bar H_x(t) = P\{T_x > t\}$, and $F_t(x) = P\{Z(t) \le x\}$ is the distribution function of the wear at time $t$.

Formalization targets

Goal: Theorem 4.10 (p. 641)

If $\{Z(t), t \ge 0\}$ satisfies (4.8), (4.9) and (4.10), then for every level $x$

$$t \longmapsto \big[\bar H_x(t)\big]^{1/t} \text{ is decreasing on } t > 0,$$

that is, $T_x$ has an IHRA distribution.

Milestones

1. Lemma 4.1b (p. 637): under (4.3)–(4.5), $[P\{X_1 + \dots + X_k \le x\}]^{1/k}$ is decreasing in $k = 1, 2, \dots$.
2. Proof of Theorem 4.10, first claim (a): for $\Delta > 0$, the grid increments $X_i = Z(i\Delta) - Z((i-1)\Delta)$ satisfy (4.3)–(4.5).
3. Proof of Theorem 4.10, first claim (b): $[F_{k\Delta}(x)]^{1/(k\Delta)}$ is decreasing in $k = 1, 2, \dots$.
4. Proof of Theorem 4.10, second claim: $[F_s(x)]^{1/s} \ge [F_t(x)]^{1/t}$ whenever $0 < s \le t$.
5. Proof of Theorem 4.10, third claim: $\bar H_x(t) = \lim_{\varepsilon \downarrow 0} F_{t+\varepsilon}(x)$, under (4.8) alone.

An optional extra item states Corollary 4.2 (4.7b): Poisson shocks of rate $\lambda > 0$ with damages satisfying (4.3)–(4.5) give an IHRA life $\bar H(t) = \sum_k e^{-\lambda t} (\lambda t)^k / k! \cdot P\{Z_k \le x\}$.

Significance

The result. Theorem 4.10 derives an ageing property of a failure time from qualitative properties of the damage process alone: no distributional form, no stationarity and no independence of increments is assumed. Together with the closure of IHRA under coherent systems, this lets a reliability engineer conclude that a system built from components failing by wear has an IHRA life. Examples include processes with nonnegative stationary independent increments started at the origin, such as compound Poisson processes and infinitesimal renewal processes (p. 641). Lemma 4.1b is the discrete analogue: a sequence of probabilities $\bar P_k$ with $\bar P_k^{1/k}$ decreasing is what Theorem 3.1 (3.4) needs to give an IHRA life under Poisson shocks.

Formalizing it. The results are proved in the paper. As far as we know none of them has been machine-checked. The formalization needs, and would make reusable, a statement of the Markov property for a continuous-time real process in terms of Mathlib's conditional expectation, versions of conditional distributions with monotonicity constraints, and the passage from a discrete-time grid to continuous time for first passage times. Each of these is a step a probabilist writes in one line and a proof assistant does not.

Difficulty

The paper's proof is short, but every sentence hides a measure-theoretic step. The first claim, that the grid increments satisfy (4.3)–(4.5), requires turning the Markov property and the monotonicity of the increment law into conditional laws of $X_{k+1}$ given $(X_1, \dots, X_k)$. Those conditional laws are defined only almost everywhere, and the monotonicity must be preserved along the way. Lemma 4.1b itself is an induction that integrates the monotonicity conditions against the law of $Z_k$. The extension from rational to arbitrary ratios $s/t$ uses the monotonicity of paths. The identification of $\bar H_x(t)$ as a right limit of $F_{t+\varepsilon}(x)$ needs the pathwise reading of (4.8). The natural first idea, approximating $Z$ by a compound Poisson process, would add hypotheses the theorem does not have.

Formalization scope

All objects sit in the namespace ShockWear.WearProcess, in one definition file. The committed conventions:

• Probability space. A measure pr with IsProbabilityMeasure. Time is $\mathbb R_{\ge 0}$; $Z : \mathbb R_{\ge0} \to \Omega \to \mathbb R$ with every $Z(t)$ measurable.
• (4.8) is read pathwise. Almost every path has $Z(0) = 0$ and is nondecreasing. The paper's "for all $t, \Delta \ge 0$ with probability one" is ambiguous in quantifier order; this reading is the one used by the proof's equivalence "$T_x > t$ iff $Z(t+\varepsilon) \le x$ for some $\varepsilon > 0$".
• (4.9) is the Markov property for the natural filtration $\sigma(Z(r), r \le s)$: $P(Z(t) \in B \mid \mathcal F_s) = P(Z(t) \in B \mid Z(s))$ a.s. for $s \le t$ and Borel $B$.
• Conditional probabilities are explicit versions. $P\{X_{k+1} \le u \mid Z_k = z\}$ and $P\{Z(t+\Delta) - Z(t) \le u \mid Z(t) = z\}$ are the values on $(-\infty, u]$ of Markov kernels $\kappa$ that agree almost everywhere with Mathlib's condDistrib. The monotonicity conditions (4.4), (4.5), (4.10) are imposed on these versions, on the paper's regions $z \ge 0$, $t \ge 0$. "Is decreasing in $z$" is read as "has a version decreasing in $z$".
• Nonnegativity of damages is almost sure.
• Index base. Lean's X i is the paper's $X_{i+1}$, and the kernel κ k describes $X_{k+1}$ given $Z_k$.
• First passage time $T_x$ takes values in $[0, \infty]$ and may be infinite with positive probability; it is not assumed finite. $\bar H_x(t) = 1$ for $t < 0$. The level $x$ ranges over all reals.
• Powers $[\,\cdot\,]^{1/t}$, $[\,\cdot\,]^{1/k}$, $[\,\cdot\,]^{1/(k\Delta)}$ are real powers with real exponents.

Trivializing formalizations are ruled out: (4.9) and (4.10) are not replaced by independence or stationarity of increments, nor by a compound Poisson model. Those are examples (p. 641), not hypotheses. Monotonicity is never imposed on Mathlib's condDistrib itself, whose values off the support of $Z(t)$ are unconstrained. A sorry-free local check confirms the hypotheses are satisfiable: the deterministic process $Z(t) = t$ satisfies (4.8)–(4.10), and constant damages satisfy (4.3)–(4.5).

Contributions are welcome on any milestone. The reduction (milestone 2) and the induction of Lemma 4.1b are the substantial parts. Lemmas about versions of conditional distributions under Markov processes would be reusable well beyond this mission.

Selected references

• J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, Ann. Probability 1(4) (1973) 627–649. https://doi.org/10.1214/aop/1176996891
• Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-out for Components and Systems, Ann. Math. Statist. 37 (1966) 816–825. https://doi.org/10.1214/aoms/1177699362
• R. C. Morey, Stochastic Wear Processes, Technical Report ORC 65-16, Operations Research Center, University of California, Berkeley, 1965 (cited on p. 640 of Esary, Marshall and Proschan).
• R. E. Barlow and F. Proschan, Statistical Theory of Reliability and Life Testing, Holt, Rinehart and Winston, 1975.