Operations Research

Motivation

Bayesian mechanism design asks which collective decisions and payments a designer can implement when every agent holds private information, the type, drawn from a commonly known prior. Most of the classical theory (Myerson's optimal auction, the Myerson–Satterthwaite impossibility, the public goods results) assumes that types are independent. Once types are correlated, as they are when bidders' values share a common component, the theory changes in a way that is best read as a paradox: Crémer and McLean (Econometrica 1988) showed that a designer can then extract the entire surplus, leaving agents no information rents. This mission formalizes Chapter 6 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press 2015), which sets up Bayesian mechanism design in general, treats independent types, and proves the Crémer–McLean theorem, together with the one numbered result of Chapter 9, the impossibility theorem of Jehiel and Moldovanu for interdependent values.

Timeline of the results formalized here:

• Rochet (1987) characterized implementable decision rules by cyclical monotonicity; Proposition 6.1 is its interim version for independent types.
• Crémer and McLean (1988): under their condition on the prior, every direct mechanism can be made Bayesian incentive-compatible without changing its decision rule or interim payments (Proposition 6.4).
• Krishna and Maenner (2001): revenue equivalence for convex type sets and convex utilities (Proposition 6.2).
• Jehiel and Moldovanu (2001): with interdependent values, efficient decisions are generically not Bayesian implementable (Proposition 9.1).
• Kosenok and Severinov (2008): an identifiability condition added to Crémer–McLean gives ex post budget balance as well (Proposition 6.6).

Setting

There are finitely many agents $i \in I$ and a set $A$ of alternatives. Agent $i$ has a type $\theta_i \in \Theta_i$ and utility $u_i(a,\theta_i) - t_i$ from alternative $a$ and payment $t_i$. Types $\theta = (\theta_1,\dots,\theta_N) \in \Theta = \prod_i \Theta_i$ are drawn from a common prior $\mu$; $\mu(\cdot\mid\theta_i)$ is the conditional distribution of the others' types $\theta_{-i}$ given $\theta_i$. Types are independent if $\mu(\cdot\mid\theta_i)$ does not depend on $\theta_i$.

A direct mechanism $(q, t_1,\dots,t_N)$ is a decision rule $q:\Theta\to A$ and payment rules $t_i:\Theta\to\mathbb R$. It is Bayesian incentive-compatible (BIC) if for every $i$ and all $\theta_i,\theta_i'$,

$$\int_{\Theta_{-i}} u_i(q(\theta_i,\theta_{-i}),\theta_i) - t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i) \ \ge\ \int_{\Theta_{-i}} u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i).$$

The interim decision rule $Q_i(\theta_i)$ is the distribution of $q(\theta_i,\theta_{-i})$ given $\theta_i$, and the interim expected payment is $T_i(\theta_i) = \int t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i)$. A mechanism is ex post budget balanced if $\sum_i t_i(\theta) = 0$ for every $\theta$, and ex ante budget balanced if $\int_\Theta \sum_i t_i\,d\mu = 0$.

In §6.4 every $\Theta_i$ is finite and $\mu(\theta) > 0$ for every $\theta$. The prior satisfies the Crémer–McLean condition if for no agent $i$ and type $\theta_i$ there are weights $\lambda \ge 0$ on $\Theta_i\setminus\{\theta_i\}$ with

$$\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_i'\ne\theta_i}\lambda(\theta_i')\,\mu(\theta_{-i}\mid\theta_i')\quad\text{for all }\theta_{-i}.$$

Identifiability requires that for every full-support distribution $\nu\ne\mu$ some agent's type $\theta_i$ has a belief $\nu(\cdot\mid\theta_i)$ that is not a nonnegative combination of the beliefs $\mu(\cdot\mid\theta_i')$.

Formalization targets

Goal: Crémer–McLean (Proposition 6.4)

If $\mu$ satisfies the Crémer–McLean condition, then for every direct mechanism $(q,t)$ there is a BIC direct mechanism $(q,t')$ with

$$\sum_{\theta_{-i}} t_i(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_{-i}} t_i'(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i)\quad\text{for all } i,\theta_i.$$

Milestones

1. Proposition 6.1 (independent types): $q$ is part of a BIC mechanism iff it is interim cyclically monotone, $\sum_{\kappa=1}^{k-1}\big(\int_A u_i(a,\theta_i^{\kappa+1})\,dQ_i(\theta_i^\kappa) - \int_A u_i(a,\theta_i^\kappa)\,dQ_i(\theta_i^\kappa)\big)\le 0$ for every cycle $\theta_i^k = \theta_i^1$.
2. Proposition 6.2 (independent types, convex type sets, convex utilities): two BIC mechanisms with $Q_i' = Q_i$ have $T_i' = T_i + \tau_i$.
3. Proposition 6.3 (independent types): every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
4. Proposition 6.5 (Farkas's alternative), already proved on the platform as Polyhedral.farkas_lemma.
5. Proposition 6.6 (Kosenok–Severinov): under Crémer–McLean and identifiability, every ex ante budget balanced mechanism has an equivalent BIC and ex post budget balanced one.
6. Proposition 9.1 (Jehiel–Moldovanu): in the linear interdependent-values model, under a regularity condition on first best rules and the weight condition $\alpha^i_{ai}/\alpha^i_{bi}\ne\sum_j\alpha^i_{aj}/\sum_j\alpha^i_{bj}$ for some $i,a,b$, no first best direct mechanism is BIC. It uses its own model (§9.3) and is not on the goal's proof path.

Significance

The Crémer–McLean theorem says that, with correlated finite types, incentive compatibility imposes essentially no constraint: every decision rule and every interim payment rule can be implemented. In a single-unit auction this gives full surplus extraction. The result is the benchmark against which the literature on risk aversion, limited liability, collusion and the genericity of priors (Robert 1991, Laffont–Martimort 2000, Heifetz–Neeman 2006) measures its departures, and Proposition 6.6 extends it to budget-balanced mechanisms, which is what bilateral trade and public goods applications need. Propositions 6.1–6.3 are the independent-types counterpart that the correlated case breaks: they show why revenue equivalence and the ex ante/ex post budget-balance equivalence hold there and fail here. Proposition 9.1 shows the opposite failure, for interdependent values, where efficient decisions cannot be implemented even without participation or budget constraints.

All results are proved in the literature (Kosenok–Severinov's proof is omitted in the book). Apart from Farkas's alternative (Proposition 6.5), which is proved on the platform, none of them is formalized in Mathlib or on the platform; the platform's other mechanism design results (dominant-strategy results in a valuation model, revenue equivalence for symmetric independent auctions) do not cover correlated types.

Difficulty

For the goal the difficulty is the uniformity of the construction: a single payment adjustment must make truth-telling optimal against every possible deviation of every type of every agent, while leaving each type's expected payment unchanged. The obvious scoring-rule adjustment, charging $-\ln\mu(\theta_{-i}\mid\theta_i')$, changes interim payments, and removing that change is where the Crémer–McLean condition enters. For Proposition 6.2 the envelope argument must handle convex type sets that are not open and utilities that are only convex, not differentiable. For Proposition 9.1 the obvious argument differentiates interim utility twice; the proposition does not assume that interim utility is twice differentiable, so that regularity has to be derived from the hypotheses on the interim probabilities.

Formalization scope

Three definition files carry the three models. Independent types (§6.2–6.3): type sets are arbitrary measurable spaces, the prior is the product of probability measures $\rho_i$, and interim quantities are integrals against it. Finite correlated types (§6.4): finite type sets, a prior $\mu:\Theta\to\mathbb R$ with $\mu(\theta)>0$ and $\sum_\theta\mu(\theta)=1$, and conditional beliefs $\mu(\theta_{-i}\mid\theta_i) = \mu(\theta)/\mu(\theta_i)$; the alternative set $A$ is arbitrary. Interdependent values (§9.3): finite $A$, signals in $[0,1]^A$ with positive densities, independent across agents, linear utilities with nonzero weights $\alpha^j_{ai}$.

Committed conventions and explicit formulas:

• The Crémer–McLean condition uses nonnegative weights without a sum-to-one constraint, as Definition 6.7 prints it.
• "Equivalent" in Propositions 6.4 and 6.6 means the same decision rule and the same interim expected payments at truthful reports, as Proposition 6.4 states; in Proposition 6.3 it is the report-by-report notion, which under independence is equality of the interim payment rules $T_i$.
• Proposition 6.2 adds continuity of $u_i(a,\cdot)$ on $\Theta_i$, and Proposition 6.3 adds at least two agents; without them the printed statements are false.
• Measurability, which the book omits throughout, is made explicit: decision rules are measurable, and the payment sections and utilities are integrable against the relevant interim distributions.
• In Proposition 9.1 the partial derivatives are derivatives within the closed cube $[0,1]^K$, and the weight condition is the displayed ratio inequality.

A trivializing formalization of the goal, one that proves it only for mechanisms that are already incentive compatible, or with a payment rule that is not a function of the reported type profile, or with "equivalent" weakened to "some BIC mechanism exists", is ruled out: the statement quantifies over every direct mechanism and fixes both the decision rule and every interim payment.

Reusable infrastructure: finite conditional expectations under a full-support prior, the Crémer–McLean and identifiability conditions, and the interim model with product priors. Proofs of any milestone and of the goal, including via the Farkas reference, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• J. Crémer and R. P. McLean, "Full extraction of the surplus in Bayesian and dominant strategy auctions", Econometrica 56(6), 1988. https://doi.org/10.2307/1913096
• G. Kosenok and S. Severinov, "Individually rational, budget-balanced mechanisms and allocation of surplus", Journal of Economic Theory 140(1), 2008.
• P. Jehiel and B. Moldovanu, "Efficient design with interdependent valuations", Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00237
• V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design", Econometrica 69(4), 2001. https://doi.org/10.1111/1468-0262.00225
• J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context", Journal of Mathematical Economics 16(2), 1987. https://doi.org/10.1016/0304-4068(87)90007-3

Why multi-stage games

Chapter X of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) carries the functional-equation method of the earlier chapters from one-player decision processes to two-player zero-sum games that are played over many stages. At each stage the two players make simultaneous choices, and those choices change the state in which the next stage is played. Games of survival are the standard example. They generalize the gambler's ruin: two players with finite resources play until one of them is ruined. The same framework is the discrete-time form of what Shapley (1953) called stochastic games. It underlies pursuit games, attrition models and the later theory of dynamic games in operations research and economics.

The chapter builds on von Neumann's min-max theorem (1928), which Bellman assumes without proof (§ 3, Eq. (3.4)). It proves three kinds of result: existence and uniqueness for the general multi-stage game equation (§§ 11–16), existence and uniqueness for games of survival with integer payoffs (§ 19), and an extended min-max theorem for ratios of bilinear forms (§ 23). Bellman proposes the ratio as a criterion for non-zero-sum games.

Setting

A matrix game is given by a real $M\times N$ matrix $A=(a_{ij})$. Player $A$ chooses row $i$ with probability $p_i$ and player $B$ chooses column $j$ with probability $q_j$; $p$ and $q$ are distribution vectors (points of the standard simplex). The expected return to $A$ is

$$E_A(p,q)=\sum_{i,j}a_{ij}\,p_i\,q_j .$$

The game has value $v$ when $\max_p\min_q E_A=v=\min_q\max_p E_A$, all extrema attained. In the Lean development this is IsMaxMinMinMaxValue, and the bilinear form is bilin.

In the general multi-stage game (§ 12) the state is a pair of vectors $P\in D\subseteq\mathbb R^n$, $P'\in D'\subseteq\mathbb R^{n'}$ with norms $\|P\|=\sum_i|P_i|$. In state $(P,P')$, $A$ chooses $u$ in a choice domain $S(P,P')$ and $B$ chooses $v$ in $S'(P,P')$. $A$ receives $R(u,v)$, and play continues from the state $T(P,P';u,v)$, $T'(P,P';u,v)$ with weight $h(P,P';u,v)$. Mixed strategies $G$, $G'$ are probability measures on the choice domains. The multi-stage game equation is

$$f(P,P')=\max_G\min_{G'}\iint\big[R(u,v)+h(P,P';u,v)\,f(T,T')\big]\,dG(u)\,dG'(v)=\min_{G'}\max_G[\ \cdots\ ].$$

A game of survival with integer payoffs (§ 19) has one integer state $x$, the resources of $A$ out of a fixed total $d$. $A$ is ruined at $x\le0$ and wins at $x\ge d$. At each stage the players play the $2\times2$ game with matrix $\begin{pmatrix}-1&a\\c&-b\end{pmatrix}$, whose entries are the transfers to $A$.

Formalization targets

Goal: the extended min-max theorem (Chapter X, Theorem 7)

For real matrices $A=(a_{ij})$, $B=(b_{ij})$ with $\sum_{i,j}b_{ij}p_iq_j\ge d>0$ for all distribution vectors $p,q$,

$$\max_p\min_q\frac{\sum_{i,j}a_{ij}p_iq_j}{\sum_{i,j}b_{ij}p_iq_j}=\min_q\max_p\frac{\sum_{i,j}a_{ij}p_iq_j}{\sum_{i,j}b_{ij}p_iq_j}.$$

It is the chapter's final result, and its statement involves only finite matrices.

Milestones

1. Eq. (3.4), von Neumann's theorem $V_A=V_B$. It is already on the platform as AGT.zero_sum_minimax (existence of a saddle point) and enters as a reference.
2. Lemma 1: the value of a one-stage game moves by at most the largest change of its kernel, $|L(f)-L_1(F)|\le\max_{u,v}\,[\,|R-R_1|+|h|\,|f(T,T')-F(T,T')|\,]$.
3. Theorem 1: under hypotheses (4a)–(4e), the multi-stage game equation has a unique solution among functions continuous on $D\times D'$ that vanish at the origin, and it is the uniform limit on bounded regions of the successive approximations.
4. Theorem 3: the successive approximations converge from any admissible initial function.
5. Theorem 4: stability, $|f(P,P')-F(P,P')|\le\sum_{n\ge0}\Delta(k^nc)$.
6. Theorem 5: the game of survival equation with boundary values $0$ and $1$ has a unique solution with values in $[0,1]$.

Significance

Theorem 7 gives a value for ratio games, the games in which a player maximizes a return per unit of a resource consumed. Bellman uses it to give a rationale for the play of non-zero-sum games (§ 24) and to derive the approximate equation (22.4) for non-zero-sum games of survival. Chapter XI, Theorem 5 generalizes it to Markovian decision processes. Theorem 1 is the existence and uniqueness result that justifies replacing an infinite game by its functional equation, and Theorems 3 and 4 make that equation usable for computation and perturbation. Theorem 5 is an early uniqueness theorem for a discrete stochastic game with absorbing boundaries.

None of these statements is formalized on the platform. Von Neumann's theorem is (AGT.zero_sum_minimax, and Sion's theorem as FamousTheorems.sion_minimax_theorem). Theorem 7 is a classical result: with a positive denominator the ratio is quasiconcave in $p$ and quasiconvex in $q$. This mission asks for a machine-checked proof of the book's statement, by Bellman's route or by any other. Theorems 1, 3 and 4 need a formal theory of games whose mixed strategies are probability measures on moving compact choice domains. No such theory is on the platform yet.

Difficulty

The ratio in Theorem 7 is not bilinear, and in general it is neither concave in $p$ nor convex in $q$, so neither von Neumann's theorem nor a concave-convex min-max theorem applies to it directly. For Theorem 1, the contraction argument needs each one-stage game to have a value and the value to depend continuously on the state. That requires a min-max theorem for continuous games on compact sets, together with continuity of the value when the choice domains move. In Theorem 5, existence follows from monotone iteration. The uniqueness step is the hard part: the operator is not a contraction in the sup norm, and a second solution must be ruled out even at states where the optimal mixed strategies are degenerate.

Formalization scope

• Distribution vectors are points of stdSimplex ℝ ι for nonempty finite types. "Max-min equals min-max" always asserts attainment (IsGreatest/IsLeast) and never uses sSup/sInf, which return $0$ on empty or unbounded sets. Theorem 7 must not assume a saddle point; its only hypothesis is the bound on the denominator.
• States are Fin n → ℝ with the $\ell^1$ norm of Eq. (12.1). Choice domains are nonempty compact sets (NonemptyCompacts), and mixed strategies are probability measures of full mass on them. "Vary continuously" in (4b), which the book does not define, is read as continuity in Mathlib's topology on nonempty compact sets (for a metric space, the topology of the Hausdorff distance).
• The maxima $w(c)$ of (4d) and $\Delta(c)$ of Theorem 4 are expressed through majorants, which is equivalent to the book's condition. $k\ge0$ is stated explicitly. In Lemma 1 the kernels are assumed measurable and bounded on $S\times S'$ so that the integrals exist, and each game having a value is a hypothesis, as in Bellman's footnote 4.
• Theorem 3's "converges" is stated as uniform convergence on bounded regions, the mode of Theorem 1, whose proof Theorem 3 repeats. Theorem 4's unspecified $c$ is any $c\ge\|P\|+\|P'\|$. The book's p. 301 prints the first min-max of Theorem 4 with the subscripts $G$, $G'$ interchanged; the equation used is that of Theorem 1.
• Theorem 5 adds the implicit $d\ge1$: for $d\le0$ the boundary conditions contradict each other. The state is an integer and $f:\mathbb Z\to\mathbb R$.
• Taking the choice domains constant would trivialize Theorem 1: condition (4d) would then force $R\equiv0$ on them. The choice domains therefore depend on the state.
• Not included: Theorem 2 (optimal strategies of the infinite game, which needs a model of the game's plays), Theorem 6 (non-zero-sum survival; the boundary conditions (21.3) do not cover all states, see the moderation notes).

Contributions of reusable infrastructure are welcome: the min-max theorem for continuous games on compact sets (Eq. (4.2)), continuity of the value in the choice domains, and value iteration for contracting game operators.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics, 2010. DOI 10.2307/j.ctv1nxcw0f
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100, 1928. DOI 10.1007/BF01448847
• L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39, 1953. DOI 10.1073/pnas.39.10.1095
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8, 1958. DOI 10.2140/pjm.1958.8.171
• I. L. Glicksberg, A further generalization of the Kakutani fixed point theorem, with application to Nash equilibrium points, Proceedings of the AMS 3, 1952. DOI 10.1090/S0002-9939-1952-0046638-5

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.

Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.

Setting

Two mines, Anaconda and Bonanza, hold amounts of gold $x \ge 0$ and $y \ge 0$. A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction $r_1$ of the gold there and stays in working order with probability $p_1$, or is destroyed without mining anything with probability $1 - p_1$. Bonanza has the corresponding data $p_2$ and $r_2$. Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.

The expected return $f(x, y)$ under an optimal policy satisfies the functional equation

$$f(x,y) = \max\Big[\,A_f(x,y),\; B_f(x,y)\,\Big], \qquad x, y \ge 0, \tag{5.1}$$

where $A_f(x,y) = p_1\big[r_1x + f((1-r_1)x,\,y)\big]$ is the return of an A-choice followed by optimal continuation and $B_f(x,y) = p_2\big[r_2y + f(x,\,(1-r_2)y)\big]$ that of a B-choice. The $N$-stage returns are $f_1(x,y) = \max(p_1r_1x,\ p_2r_2y)$ and $f_{N+1} = \max(A_{f_N}, B_{f_N})$. The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.

In the generalization, a use of mine $i$ has $K$ outcomes: outcome $k$ occurs with probability $p_{ik}$, yields $c_{ik}x_i$ and leaves $c'_{ik}x_i = (1-c_{ik})x_i$ in the mine, and $1 - \sum_k p_{ik}$ is the probability that the machine is destroyed. With $n$ mines the equation is

$$f(x_1,\dots,x_n) = \max_i \sum_{k=1}^{K} p_{ik}\big[c_{ik}x_i + f(x_1,\dots,c'_{ik}x_i,\dots,x_n)\big]. \tag{4}$$

"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle $0 \le x \le \bar X$, $0 \le y \le \bar Y$ (or every box $0 \le x_i \le \bar X_i$), per Bellman's footnote 7.

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Under $p_{ik} \ge 0$, $\sum_k p_{ik} < 1$, $0 \le c_{ik} \le 1$, $c_{ik} + c'_{ik} = 1$, equation (4) has a unique solution bounded on boxes, and at every state $x$ any index maximizing

$$D_i(x) = \frac{\sum_{k} p_{ik}c_{ik}}{1-\sum_{k} p_{ik}}\;x_i$$

attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.

Milestones

1. Theorem 1: for $|p_i| < 1$ and $0 \le r_i < 1$, (5.1) has a unique solution bounded in every rectangle, and it is continuous on the closed quadrant.
2. Theorem 2: for $0 \le p_i < 1$, $0 \le r_i \le 1$, the solution takes the A-branch when $p_1r_1x/(1-p_1) > p_2r_2y/(1-p_2)$, the B-branch when the reverse inequality holds, and both on equality.
3. Theorem 3: the same rule for two mines with $K$ outcomes per use.
4. Theorem 5: for each $N$, the $N$-stage process has exactly two decision regions: a sector along the $x$-axis where A is optimal and a sector along the $y$-axis where B is optimal, separated by a ray through the origin.
5. Theorem 6: as $N$ grows, the regions of $f_N$ move monotonically, and from some $N_0$ on they coincide with those of $f$.
6. Theorem 7: if $g$ solves (5.1) with an added term $h$, then $|f - g| \le \max_R|h|/q$ on every rectangle $R$, where $q = \min(1-p_1, 1-p_2)$.

Significance

The index rule reduces the choice among $n$ mines to computing $n$ numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the $N$-stage process is a word in $n$ letters whose number of candidates grows like $n^N$. The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite $N_0$, and the stability theorem bounds how much the solution moves when the equation is perturbed.

Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The $n$-mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.

Difficulty

The equation for the boundary between the regions involves the unknown function $f$, so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of $f_N$ generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.

Formalization scope

Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with $n \ge 1$ added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's $N$). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most $f(x)$ and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for $n$ mines it is BoundedOnBoxes. The $N$-stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's $f_1$.

Choices made explicit:

• Theorem 1 keeps the book's signed range $|p_i| < 1$ (footnote 2), while Theorems 2, 5, 6 and 7 use the range of § 8 and Theorem 2, $0 \le p_i < 1$, $0 \le r_i \le 1$.
• The goal asserts existence and uniqueness of the bounded solution of (4) together with the index rule. This is how "the solution" is meant in the book; the extension of Theorem 1 to (4) is not a separate numbered result.
• The goal's conclusion is the book's: a maximizer of $D$ is optimal. It does not also assert that the other indices are suboptimal.
• Theorem 5's printed statement is only "there are two decision regions". It is formalized as the ray-separation statement its proof establishes, and is titled as the precise reading. Theorem 6's "converge in a monotone fashion" is formalized as monotonicity of the regions as sets, in one of the two directions.
• Theorem 7 adds the hypothesis that $h$ is bounded in every rectangle, which is what gives the perturbed equation a solution in the class. $\max_R|h|$ is expressed through any bound $M$ of $|h|$ on $R$.

A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).

Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.

Selected references

• Richard Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter II, pp. 61–80. https://doi.org/10.2307/j.ctv1nxcw0f
• Richard Bellman, The theory of dynamic programming, Bulletin of the American Mathematical Society 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
• J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society, Series B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$, $T_{iG}\ge 1$ is the first passage time to $G$. The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$. The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$. The mean first passage time is $m_{iG}=E[T_{iG}]$, infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$. A state $i$ is positive recurrent when $m_{ii}<\infty$, and the steady state probability is $\pi_i=m_{ii}^{-1}$. On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$. The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$. Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$, and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$, a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$. The quantities of $\Gamma_N$ are written $m_{iG}(N)$, $c_{iG}(N)$, $\pi_i(N)$ and $J(i)(N)$. An AS is conforming (for a $z$ standard $\Gamma$) if, for large $N$, $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$. It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$:

$$P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.$$

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$.

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$,

$$\text{every ATAS that sends excess probability to } G \text{ is conforming},$$

and if $G\subseteq R$ it is also conforming on $R$. No rate of convergence and no constants are involved, and $G$ need not contain $z$.

Milestones

1. Proposition C.4.2: for fixed $t$, $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$.
2. Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$.
3. Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$.
4. Proposition C.4.6: on a positive recurrent class, convergence of $\pi$, of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$, of $c_{zz}$ and of all $c_{iG}$ are equivalent.
5. Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$, and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$.

Further results

6. Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$, the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$.
7. Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$, the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$. First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$, a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$, and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$, $c_{iG}$, $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$. $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$, the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$. $\Gamma_N$ is built as an MC on the subtype of $S_N$, and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$. Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ($N<N_0$ or a state outside $S_N$). For fixed states this affects finitely many $N$, and all statements are limits, $\liminf$s or eventual equalities. All convergence is in $[0,\infty]$. The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$.

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$, is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$, and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
• L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
• L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
• D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).