The OR Formalization Drive

Motivation

Little's law $L = \lambda W$ says that the long-run average number of customers in a system equals the arrival rate times the average time a customer spends there. It is one of the most used identities in queueing theory, and it holds on individual sample paths under weak conditions (Little 1961; Stidham 1974). Many quantities of interest are not head counts, however: the work in the system, the cost accumulated by customers in progress, the number of tokens a customer holds in some state. For these a more general relation is needed, between a time average $H$ and a customer average $G$, of the form $H = \lambda G$.

Heyman and Stidham (Oper. Res. 28 (1980)) prove such a relation on each sample path, for an arbitrary real-valued function attached to each customer, under a support condition that is much weaker than the continuous-sojourn assumption of the $L = \lambda W$ theorem. They then show by a counterexample that the support condition cannot simply be dropped, even when every customer function is an indicator.

Timeline.

• 1961: Little proves $L = \lambda W$ under stationarity assumptions (Little 1961).
• 1971: Brumelle proves $H = \lambda G$ under conditions (v.a), (v.b) on the tails of the $f_n$ (J. Appl. Prob. 8, 508–520).
• 1972: Stidham gives a new proof of $L = \lambda W$, including the lemma relating $N(t)/t$ and $t_n/n$ (Stidham 1972).
• 1974: Stidham proves $L = \lambda W$ on each sample path, assuming each sojourn is one uninterrupted interval (Stidham 1974).
• 1980: Heyman and Stidham prove $H = \lambda G$ on every sample path under the support condition below, and give the counterexample. The paper notes that its Theorem 1 is weaker than the sample-path version of Brumelle's theorem, with hypotheses stated directly on the sample path.

Setting

Fix one sample path. Customers $n = 1, 2, \ldots$ arrive at epochs $0 \le t_1 \le t_2 \le \cdots$; ties are allowed. The arrival count $N(t)$ is the number of $n$ with $t_n \le t$, and the arrival rate is $\lambda = \lim_{t\to\infty} N(t)/t$ when the limit exists.

Customer $n$ carries a real-valued function $f_n$ on $[0,\infty)$. Its total is $g_n = \int_0^\infty f_n(t)\,dt$, and the rate is $h(t) = \sum_{n=1}^\infty f_n(t)$. The customer average and time average are

$$G = \lim_{N\to\infty} \frac1N \sum_{n=1}^N g_n, \qquad H = \lim_{T\to\infty} \frac1T \int_0^T h(t)\,dt .$$

When $f_n$ is the indicator of $[t_n, t_n + W_n)$, $g_n = W_n$ is the sojourn time and $h(t)$ is the number in system, so $H = \lambda G$ is $L = \lambda W$.

The ASSUMPTION of the paper is that for each $n$ there is $s_n \in [0,\infty)$ with

1. (i) $f_n(t) = 0$ for $t \notin [t_n, t_n + s_n]$;
2. (ii) $s_n / n \to 0$.

For signed $f_n$ write $f_n^+ = \max[0, f_n]$, $f_n^- = \max[0, -f_n]$, and let $g_n^\pm$, $h^\pm$, $G^\pm$, $H^\pm$ be the corresponding totals, rates and averages.

Formalization targets

Goal: Theorem 2 (p. 986)

Assume (i), (ii) and (v) $\int_0^\infty |f_n(t)|\,dt < \infty$ for every $n$. If $\lambda$, $G^+$ and $G^-$ exist with $0 < \lambda < \infty$ and $G^\pm < \infty$, then $G$ exists, equals $G^+ - G^-$, $H$ exists, and

$$H = \lambda G. \tag{1}$$

Milestones

• (2): for $0 < \lambda < \infty$, $N(t)/t \to \lambda$ if and only if $t_n / n \to \lambda^{-1}$.
• (3): for $f_n \ge 0$, $V(T) \le \int_0^T h(t)\,dt \le U(T)$, where $U(T)$ sums $g_n$ over arrived customers and $V(T)$ over customers with $t_n + s_n \le T$.
• (4): $\lambda G = \lim_{t\to\infty} U(t)/t$.
• $s_n / t_n \to 0$, and $\lim U(t)/t = \lim V(t)/t$.
• Theorem 1 (p. 985): for $f_n \ge 0$ under (i)–(iv), $H = \lambda G$.
• The identity $\int_0^T h^+ - \int_0^T h^- = \int_0^T h$ and (6): $G = G^+ - G^-$, $H = H^+ - H^-$.

Companion results

• The §3 counterexample: $t_n = n$, indicator $f_n$ with $g_n = 1$, so $\lambda = G = 1$, but $H = \log 2$; its support span $s_n = n$ satisfies (i) and fails (ii).
• Corollary 3 (p. 988): if $\lambda(\omega) = \lambda$ is constant, the ensemble averages satisfy $\int H\,dP = \lambda \int G\,dP$.
• $G = W < \infty$ implies $W_n / n \to 0$ (p. 986), the step by which Theorem 1 contains $L = \lambda W$.

Significance

The result. $H = \lambda G$ converts between a time average, which is what a system designer measures, and a customer average, which is what a customer experiences. Applied to different $f_n$ it yields $L = \lambda W$, the relation between average work in system and average customer work, and relations between time-stationary and embedded-chain probabilities; §2 of the paper derives the GI/M/c/K relation this way. Because the support condition (i)–(ii) allows a customer's contribution to be interrupted (leaving and re-entering the system), it covers preemptive priority queues and nodes of networks, which the continuous-sojourn $L = \lambda W$ theorem does not. The counterexample marks the boundary: with interrupted sojourns, indicator functions and finite $\lambda$, $G$ alone do not suffice.

Formalizing it. The result is proved on paper, with two steps delegated to earlier work "by mimicking" Lemma 1 and Theorem 2 of Stidham 1974. The indicator special case $L = \lambda W$ (with strictly increasing arrivals) is already proved on Prove2Me as queueing_general_littles_law (wenxinzhang). This mission asks for the general, signed, pathwise statement and its proof steps, a counterexample with an exactly computed time average $\log 2$, and the ensemble corollary.

Difficulty

The obvious argument, exchanging the time integral of $h$ with the sum over customers, gives $\int_0^T h = \sum_n \int_0^T f_n$, but a customer that has arrived by $T$ may contribute only part of its total $g_n$ by $T$. The sandwich $V(T) \le \int_0^T h \le U(T)$ only bounds this loss; the hard step is showing that $U(t)/t$ and $V(t)/t$ have the same limit, which needs $s_n / t_n \to 0$ to compare $V$ at time $t$ with $U$ at a slightly earlier time. Without (ii) this fails, as the counterexample shows: customers there remain "open" for a window proportional to their index.

For signed $f_n$ the sandwich is not available directly, and the proof splits $f_n$ into positive and negative parts; the exchange of sum and integral then needs the finiteness of the parts on every $[0,T]$.

Formalization scope

All statements except Corollary 3 are about one fixed sample path; the paper's "with probability one" is the pathwise statement applied to almost every path, and Corollary 3 states this explicitly with a probability measure and almost-sure hypotheses.

Conventions:

• Customers are indexed from $0$ in Lean; index $n$ is the paper's customer $n+1$, so $s_n/n \to 0$ is written $s_n/(n+1) \to 0$.
• Arrival epochs are Monotone with $t_0 \ge 0$; ties are allowed.
• $f_n : \mathbb R \to \mathbb R$, but only values on $[0,\infty)$ enter: (i) is required only for $t \ge 0$, $g_n$ integrates over $[0,\infty)$, and time averages integrate over $[0,T]$.
• (iv) and (v) are stated as integrability of $f_n$ on $[0,\infty)$; the page prints (iv) as "$\le \infty$", a misprint for "$< \infty$".
• $N(t)$ is the cardinality of $\{n : t_n \le t\}$; $h$, $U$, $V$ are infinite sums over all customers.
• "$H$ exists" includes integrability of $h$ on every $[0,T]$.
• The page prints (6) as "$G = G^+ - G^+$"; the stated identity is $G = G^+ - G^-$, as the proof shows.

Added hypotheses: milestones (3), the $h^\pm$ identity and (6) assume $t_n \to \infty$, which the paper derives from (2); Corollary 3 assumes $G(\omega)$ is integrable, which its definition of the ensemble average presupposes.

A formalization in which $h$ sums only over arrived customers, or in which a non-integrable $h$ or $f_n$ has integral $0$, would make the statements trivial or different; the definitions rule this out by summing over all customers and requiring integrability.

Needed infrastructure: Cesàro averages and counting functions of nondecreasing sequences, interchange of countable sums and integrals for locally finite families, and harmonic sums $\sum_{m=\lceil (k+1)/2\rceil}^{k} 1/m \to \log 2$. The counting-function lemma (2) and the squeeze for $U$ and $V$ are reusable well beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• D. P. Heyman and S. Stidham, Jr., The relation between customer and time averages in queues, Operations Research 28(4):983–994, 1980. https://doi.org/10.1287/opre.28.4.983
• J. D. C. Little, A proof for the queuing formula: L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
• S. Stidham, Jr., L = λW: a discounted analogue and a new proof, Operations Research 20(6):1115–1126, 1972. https://doi.org/10.1287/opre.20.6.1115
• S. Stidham, Jr., A last word on L = λW, Operations Research 22(2):417–421, 1974. https://doi.org/10.1287/opre.22.2.417
• S. L. Brumelle, On the relation between customer and time averages in queues, Journal of Applied Probability 8:508–520, 1971.

Linear programs for average-reward Markov decision chains

A Markov decision chain is a controlled Markov chain: in each state the controller picks an action, collects a reward and moves to a random next state with probabilities that depend on the state and the action. Under the average reward criterion, the long-run reward per step, an optimal policy can be computed by linear programming. For chains in which every stationary policy has a single recurrent class (the unichain case) this goes back to Manne (1960), de Ghellinck (1960) and d'Epenoux (1960): the variables of the dual linear program are long-run state–action frequencies, and the vertices of its feasible set are exactly the pure stationary policies.

In the general multichain case a policy may split the state space into several recurrent classes with transient states between them, and the frequency picture breaks down. Denardo and Fox (1968) and Denardo (1970) gave linear programs that require solving several programs in sequence. Hordijk and Kallenberg (Management Science 25(4), 1979) showed that one pair of dual linear programs suffices: from an optimal dual solution one reads off an average optimal policy (their Theorems 7 and 8). To make the correspondence between policies and dual solutions explicit, they attach to every stationary policy a representative, a particular feasible solution of the dual program, and prove (Theorem 10) that the representative of a pure stationary policy is a vertex of the feasible set. This mission formalizes Theorem 10.

Timeline:

• 1960: Manne; de Ghellinck; d'Epenoux. The linear program for unichain average-reward problems, with pure policies at the vertices.
• 1962: Blackwell. The limit matrix $P^*$ and deviation matrix $D$ of a finite stochastic matrix, and their identities (Ann. Math. Statist. 33).
• 1968–1970: Denardo and Fox; Denardo. Multichain problems by a sequence of linear programs.
• 1979: Hordijk and Kallenberg. A single dual pair for the multichain case; representatives of stationary policies; Theorem 10.

Setting

The state space $E$ is finite. Each state $i$ has a finite nonempty set $A(i)$ of actions; action $a$ in state $i$ earns $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$, $\sum_j p_{iaj}=1$. Fix weights $\beta_j>0$ with $\sum_j\beta_j=1$.

The dual linear program has one pair of variables $x_{ia},y_{ia}$ for each state $i$ and each admissible action $a\in A(i)$. Its feasible set consists of the $(x,y)$ with

$$\textstyle\sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\qquad \sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\qquad(j\in E),\qquad x,y\ge 0 .$$

A pure stationary policy $f^\infty$ uses the action $f(i)\in A(i)$ whenever the chain is in state $i$. Its transition matrix is $P(f)=(p_{if(i)j})$. For a stochastic matrix $P$, the limit matrix $P^*=\lim_n\frac1n\sum_{k=1}^nP^{k-1}$ exists, and the deviation matrix is $D=(I-P+P^*)^{-1}-P^*$. A state is recurrent if every state reachable from it can reach it back, and transient otherwise; the set $T$ collects the transient states, and the states reachable from a recurrent state form an ergodic set. Write $E_1,\dots,E_m$ for the ergodic sets of $P(f)$.

The representative of $f^\infty$ is

$$x_{ia}(f)=[\beta^TP^*(f)]_i\,\delta_{af(i)},\qquad y_{ia}(f)=[\beta^TD(f)+\gamma^TP^*(f)]_i\,\delta_{af(i)},$$

with $\gamma_l=0$ for $l\in T$ and, for $l\in E_j$, $\gamma_l=\max_{i\in E_j}\big(-\sum_k\beta_kd_{ki}\big)\big/\sum_{k\in E_j}p^*_{ki}$. The paper defines the same formulas for randomized stationary policies $\pi$, with $\pi_{ia}$ in place of $\delta_{af(i)}$.

Formalization targets

Goal: Theorem 10 (p. 361)

$$(x(f),y(f))\ \text{is an extreme point of the feasible set of the dual linear program}$$

for every finite Markov decision chain, every positive probability vector $\beta$ and every pure stationary policy $f^\infty$. The statement contains feasibility of the representative.

Milestones

1. §3.3, pp. 359–360: the representative $(x(\pi),y(\pi))$ of any stationary policy is feasible.
2. Proof of Theorem 10, p. 362: for a stochastic $P$, every solution of $x^T(I-P)=0$, $x^T+y^T(I-P)=\beta^T$ (system (7)) satisfies $x^T=\beta^TP^*$ and $y^T=\beta^TD+y^TP^*$.
3. Proof of Theorem 10, p. 362: such a solution has $y_i=(\beta^TD)_i$ for $i\in T$.
4. Proof of Theorem 10, p. 362: on each ergodic set $E_k$ of $P(f)$ there is a state $i(k)$ with $y_{i(k)f(i(k))}(f)=0$.
5. Proof of Theorem 10, p. 362 (Chung, p. 33): a row vector $z$ with $z_i=\sum_{l\in E_k}z_lp_{li}$ on an ergodic set $E_k$ that vanishes at one state of $E_k$ vanishes on all of $E_k$.

Significance

Theorem 10 is the vertex half of the policy–solution correspondence of Hordijk and Kallenberg: every pure stationary policy appears as a basic feasible solution of one linear program, in the multichain case and without any communication assumption. It connects the simplex method on that program with the set of pure policies, and it is a building block for the later literature on linear programming for multichain Markov decision problems. The paper also records that the converse fails: an extreme point may induce a randomized policy.

The result is proved in the paper. As far as is known it has not been machine-checked. A formal proof also checks the exact form of $\gamma$: the paper prints the denominator of $\gamma_l$ as $\sum_k p^*_{ki}$, a sum over all states, and with that reading the representative is not feasible as soon as transient states feed an ergodic set (two states, $0\to1\to1$: $y_1=-\beta_0/2$). The denominator $\sum_{k\in E_j}p^*_{ki}$ is the one the paper's own feasibility computation on p. 360 uses, and it is the one stated here.

Difficulty

Feasibility is a calculation with the identities $PP^*=P^*P=P^*P^*=P^*$ and $(I-P)D=I-P^*$. Extremality is the substance. Restricted to the pairs $(i,f(i))$, the constraints become the square system (7) in the state variables, and system (7) determines $x$ and the transient part of $y$, but on each ergodic set it determines $y$ only up to adding a multiple of the stationary distribution of that class: the matrix $I-P$ is singular, with one degree of freedom per ergodic set. The naive argument, that the equality constraints alone pin the point down, therefore fails as soon as there is an ergodic set; the extra information has to come from the nonnegativity constraints, and that is why the exact value of $\gamma$ matters. In the general multichain setting this requires the class structure of a finite Markov chain (closed classes, transient states, the support of $P^*$, uniqueness of invariant vectors on a closed communicating class), little of which is in Mathlib in usable form.

Formalization scope

• The model is the published MarkovDecisionProcesses.StationaryMDP: finite states, finite actions, admissible sets $A(i)$ (nonempty), transition probabilities nonnegative with unit row sums. $P^*$ and $D$ are the published limitMatrix and deviationMatrix of Blackwell's Lemma 1, whose identities are the open platform theorems BlackwellDiscreteDP.NearOne.lemma_1a and lemma_1d.
• The dual variables are functions on the subtype of admissible state–action pairs, so non-admissible actions have no coordinates. The feasible set is a subset of $(\mathrm{Pair}\to\mathbb R)\times(\mathrm{Pair}\to\mathbb R)$ and "extreme point" is Mathlib's Set.extremePoints ℝ. Membership in it includes feasibility.
• Row vectors act by vecMul. Recurrence and accessibility are the published IsRecurrent and Accessible; the ergodic set of a recurrent $l$ is the set of states accessible from $l$. The maximum in $\gamma$ is a Finset.sup' over that finite nonempty set.
• $\gamma$ uses the corrected denominator $\sum_{k\in E_j}p^*_{ki}$. A formalization with $\gamma=0$, or one in which the non-admissible coordinates of the program are free, is a different and false or trivial statement and is ruled out.
• Stationary randomized rules are nonnegative weights on $A(i)$ summing to one; the pure rule of $f$ is the indicator of $f(i)$.
• Useful contributions: the class decomposition of a finite stochastic matrix (closed classes, $p^*_{ki}=0$ for transient $i$, positivity of $p^*_{ii}$ on recurrent states), uniqueness of invariant vectors on a closed communicating class, and proofs of Blackwell's Lemma 1(a), 1(d). All of these are reusable beyond this mission.

Selected references

• A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
• E. V. Denardo, On Linear Programming in a Markov Decision Problem, Management Science 16(5):281–288, 1970. https://doi.org/10.1287/mnsc.16.5.281
• E. V. Denardo and B. L. Fox, Multichain Markov Renewal Programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968. https://doi.org/10.1137/0116038
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259

Motivation

A Markov decision chain with finitely many states and actions is the basic model of sequential decision making under uncertainty in operations research. Inventory control, maintenance, queueing control and many other problems reduce to it. Under the average reward criterion the decision maker optimizes the long-run reward per period. For the discounted criterion one linear program yields an optimal pure stationary policy (d'Epenoux 1960). For the average criterion, De Ghellinck (1960) and Manne (1960, DOI 10.1287/mnsc.6.3.259) gave linear programs for the unichain case, where every stationary policy has a single recurrent class. In a multichain model the optimal average reward may differ from state to state, and the unichain construction no longer applies.

Hordijk and Kallenberg (Management Science 25(4):352–362, 1979, DOI 10.1287/mnsc.25.4.352) proved that in the general multichain case an average optimal policy can be found by solving only one linear program. This mission formalizes that result, Theorem 7 of the paper, together with the chain of results its proof rests on.

Timeline, following the paper's introduction:

• 1960: d'Epenoux introduces linear programming for the discounted case; De Ghellinck and Manne treat the unichain average case.
• 1962: Blackwell (DOI 10.1214/aoms/1177704593) proves that some pure stationary policy is discounted-optimal for all discount factors near 1, and expands the discounted value near $\alpha = 1$.
• 1968–1970: Denardo and Fox (DOI 10.1137/0116038) and Denardo (DOI 10.1287/mnsc.16.5.281) give the first analysis of linear programs for the multichain case. Derman's 1970 monograph streamlines it: in the worst case two linear programs and one search problem must be solved. Denardo and Fox record Bruce Miller's conjecture that the policy of Theorem 7 below is optimal.
• 1979: Hordijk and Kallenberg prove the conjecture (Theorem 7), so one linear program suffices.

Setting

The state space is a finite nonempty set $E$. In state $i$ a finite nonempty set $A(i)$ of actions is available; choosing $a \in A(i)$ earns the reward $r_{ia}$ and moves the system to state $j$ with probability $p_{iaj}$ ($p_{iaj} \ge 0$, $\sum_j p_{iaj} = 1$). A policy $R$ chooses actions at times $t = 1, 2, \dots$, possibly at random and using the whole history. For a policy $R$ and an initial state $i$,

$$\varphi_i(R) = \liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a \mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}$$

is the average expected reward, and $\varphi_i = \sup_R \varphi_i(R)$ is the optimal one. A policy $R^*$ is average optimal if $\varphi_i(R^*) = \varphi_i$ for every $i \in E$. A decision rule $f$ picks $f(i) \in A(i)$ in every state; $f^\infty$ is the pure stationary policy that always applies $f$. Its transition matrix is $P(f) = (p_{if(i)j})$ and its reward vector $r(f) = (r_{if(i)})$. The α-discounted value $v_i^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\sum_j\sum_a\mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}$ enters through Theorems 1, 3, 4 and 5.

Fix weights $\beta_j > 0$ with $\sum_j \beta_j = 1$. The dual program has a variable pair $x_{ia}, y_{ia}$ for every state $i$ and every $a \in A(i)$:

$$\max \sum_i\sum_a r_{ia}x_{ia}\quad\text{s.t.}\quad \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\quad \sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j,\quad x,y\ge0,$$

for all $j \in E$. Its linear programming dual, the primal program, minimizes $\sum_j\beta_j\tilde\varphi_j$ over superharmonic pairs $(\tilde\varphi,\tilde u)$: $\tilde\varphi_i \ge \sum_j p_{iaj}\tilde\varphi_j$ and $\tilde\varphi_i + \tilde u_i \ge r_{ia} + \sum_j p_{iaj}\tilde u_j$ for all $a \in A(i)$, $i \in E$. For a dual solution $(x, y)$ put $E_x = \{i \mid \sum_a x_{ia} > 0\}$.

Formalization targets

Goal: Theorem 7

Let $(x, y)$ be an optimal solution of the dual program that is an extreme point of its feasible set, which is what the simplex method returns. Let $f$ be any decision rule with

$$x_{if(i)} > 0 \ \ (i \in E_x), \qquad y_{if(i)} > 0 \ \ (i \notin E_x).$$

Then $f^\infty$ is average optimal: $\varphi_i(f^\infty) = \varphi_i$ for every $i \in E$, the comparison running over all policies.

Milestones

In the order the proof uses them:

1. Theorem 1 (Blackwell): some pure stationary $f_0^\infty$ is α-discounted optimal for all α near 1.
2. Theorem 2a: $\varphi(f^\infty) = P^*(f)r(f)$. The other clauses of Theorem 2 are Blackwell's Lemma 1(a), (d), referenced as published theorems.
3. Theorem 3 (Blackwell): $v_i^\alpha(f^\infty) - \varphi_i(f^\infty)/(1-\alpha) \to (D(f)r(f))_i$ as $\alpha \uparrow 1$.
4. Theorem 4 (Derman): the policy of Theorem 1 is average optimal.
5. Theorem 5: $\varphi^0 = \varphi(f_0^\infty)$ and $u^0 = D(f_0)r(f_0)$ solve the two nested optimality equations.
6. Proof of Theorem 6: $(\varphi^0, u^0 + M\varphi^0)$ is superharmonic for some $M$.
7. Theorem 6: $\varphi$ is the smallest function that admits $u$ with $(\varphi, u)$ superharmonic.
8. §3.2: $(\varphi(f_0^\infty), D(f_0)r(f_0) + M\varphi(f_0^\infty))$ is primal optimal for all large $M$.
9. Proof of Theorem 7: $\sum_a x_{ja} + \sum_a y_{ja} \ge \beta_j > 0$, so the rule always defines a policy; and every primal optimum has first component $\varphi$.
10. Propositions 1–3: $\varphi$ is $P(f)$-harmonic and the gain–bias equation holds on $E_x$; $E_x$ is closed under $P(f)$; at an extreme optimal dual solution, the states outside $E_x$ are transient under $P(f)$.

Significance

Theorem 7 turns the multichain average-reward problem into one linear program and one pass over its solution. No unichain or communicating assumption is required, and neither the second linear program nor the search step of the earlier Denardo–Fox–Derman procedure is needed. The rule is local: any action with a positive $x$-variable, otherwise any action with a positive $y$-variable, gives an optimal policy. The paper's later results (Theorem 8, the correspondence between optimal dual solutions and optimal randomized stationary policies, and Theorem 10, on extreme points) build on the same program. Companion missions of this series formalize them.

The results are proved in the paper; no machine-checked proof of any of them is known. The formalization adds a machine-checked link between linear programming duality (complementary slackness, extreme points of polyhedra) and the limit theory of finite Markov chains (Cesàro limit matrices, transient states), over the history-dependent policy class of the published average-reward model.

Difficulty

The obvious argument reads $f$ off any optimal dual solution and uses complementary slackness to obtain $\varphi = P(f)\varphi$ and $\varphi + (I - P(f))u = r(f)$. The second equation holds only on $E_x$, and outside $E_x$ nothing controls the reward of $f$. The argument closes only when $E \setminus E_x$ is transient under $P(f)$, so that the stationary distribution of $f$ ignores those states. Transience is not a consequence of optimality. It uses extremality: an ergodic set inside $E\setminus E_x$ would make the corresponding $y$-columns of the constraint matrix linearly dependent. For a general optimal solution the paper proves optimality only of a randomized stationary policy built from $(x, y)$ (its Theorem 8(b), a companion mission), not of a pure selection. The extremality hypothesis is therefore part of the statement.

Upstream of the linear program, Theorem 6 depends on Derman's theorem and Blackwell's expansion of the discounted value near $\alpha = 1$. Both compare against all history-dependent policies and need the full limit theory of $P^*$ and $D$.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP (finite nonempty S, finite A, nonempty admissible sets, stochastic transitions) with history-dependent randomized policies AvgHRPolicy. $\varphi_i(R)$ is gainInf (the lim inf of the average of the first $T$ expected rewards) and $\varphi_i$ is optGainInf, a real supremum that is finite because rewards are bounded. $P^*$ and $D$ are the published limitMatrix and deviationMatrix; the identities of Theorem 2 are the published Blackwell Lemma 1(a), (d). Conventions:

• Average optimality is Hordijk and Kallenberg's $\varphi(R^*) = \varphi$, not the stronger Puterman criterion IsAverageOptimal in the published file.
• The discounted value is the limit of the $N$-epoch discounted reward, defined by the same backward recursion as totalReward. "α near enough to 1" means some $\alpha_0 \in [0,1)$ such that the property holds on $[\alpha_0, 1)$.
• Dual variables are indexed by the admissible pairs only (Pair M), so the feasible set lies in (Pair M → ℝ) × (Pair M → ℝ) and its extreme points are those of the paper's polyhedron.
• "The simplex method is used" is encoded as "$(x, y)$ is an extreme point of the feasible set" (Set.extremePoints). A goal without extremality is a different and unproved statement, and any version that quantifies over some $f$ instead of every $f$ obeying the rule is weaker than the paper's. Both are ruled out.
• "Transient" is the negation of the published IsRecurrent. Maxima over $A(i)$ and $A^0(i)$ are stated as an upper bound plus attainment, so that $A^0(i) \ne \emptyset$ is part of Theorem 5.

A complete development needs Cesàro limits of stochastic matrices, the deviation matrix, Abelian limits of discounted values, linear programming duality with complementary slackness, and the characterization of extreme points of $\{z \ge 0 : Az = b\}$ by linear independence of the active columns. The last two are reusable well beyond this mission, as is the identification of gainInf of a stationary policy with $P^*r$. Contributions to any of them, including proofs of individual milestones, are welcome.

Selected references

• A. Hordijk, L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• E. V. Denardo, On Linear Programming in a Markov Decision Problem, Management Science 16(5):281–288, 1970. https://doi.org/10.1287/mnsc.16.5.281
• E. V. Denardo, B. L. Fox, Multichain Markov Renewal Programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968. https://doi.org/10.1137/0116038
• J. G. Kemeny, J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• C. Derman, Finite State Markovian Decision Processes, Academic Press, 1970.

Motivation

Reliability theory classifies life distributions by how they age. A device whose remaining life, once it has survived to age $t$, is stochastically shorter than the life of a new device is called new better than used (NBU). The NBU class, together with the classes IHR (increasing hazard rate) and IHRA (increasing hazard rate average), organizes much of the theory of maintenance and replacement: Marshall and Proschan showed that the NBU property is what makes certain replacement policies beneficial, and Barlow and Proschan's monographs build the statistical theory of reliability on these classes.

A question that runs through this literature is where such ageing properties come from physically. Esary, Marshall and Proschan (Ann. Probability 1973) answer it for shock models: a device is hit by shocks arriving in time as a Poisson process, each shock adds a random amount of damage, and the device fails when the accumulated damage exceeds its threshold. Section 4 of their paper treats a fixed threshold and shows that the life is IHRA for every damage law. Section 5, the subject of this mission, lets the threshold itself be random, which models the variation between individual items of a production lot. It then asks which ageing properties of the threshold law are inherited by the life distribution, and which are forced if the inheritance is to hold whatever the damage law.

Setting

All distributions are laws of non-negative random variables. For a distribution $F$ on $\mathbb R$ with $F(z) = 0$ for $z < 0$ (a damage law), $F^{(k)}$ denotes the $k$-fold convolution of $F$, with $F^{(0)}$ the point mass at $0$; thus $F^{(k)}(x) = P\{X_1 + \cdots + X_k \le x\}$ for independent $X_i \sim F$.

A threshold law is a distribution $G$ with $G(z) = 0$ for $z < 0$; write $\bar G = 1 - G$ for its survival function. If the threshold $Y \sim G$ is independent of the damages, the probability of surviving $k$ shocks is

$$\bar P_k = \int_0^\infty F^{(k)}(x)\, dG(x) = P\{X_1 + \cdots + X_k \le Y\}, \qquad k = 0, 1, \dots \tag{5.1}$$

If shocks arrive as a Poisson process of rate $\lambda > 0$, the device's life distribution $H$ has survival function

$$\bar H(t) = \sum_{k=0}^\infty e^{-\lambda t}\frac{(\lambda t)^k}{k!}\,\bar P_k, \qquad t \ge 0. \tag{5.2}$$

A survival function $\bar F$ is NBU if $\bar F(t + x) \le \bar F(x)\bar F(t)$ for all $x, t \ge 0$; it is IHR if $\bar F(x + t)/\bar F(t)$ is non-increasing in $t$ for each $x > 0$, and IHRA if $[\bar F(t)]^{1/t}$ is non-increasing in $t > 0$. The discrete analogue of NBU for the sequence $\bar P_k$ is submultiplicativity, $\bar P_{j+k} \le \bar P_j \bar P_k$.

Formalization targets

Goal: Theorem 5.3

For a threshold law $G$ with $G(z) = 0$ for $z < 0$:

$$\Big(\forall F:\ \bar P_{j+k} \le \bar P_j\,\bar P_k \ \ \forall j,k \ge 0\Big) \iff \bar G \text{ is NBU},$$

the quantifier ranging over every damage law $F$; and if $G$ is NBU, then for every damage law $F$ and every $\lambda > 0$ the life distribution $H$ of (5.2) is NBU.

Milestones

1. Theorem 3.1 (3.5). For any sequence $1 = \bar P_0 \ge \bar P_1 \ge \cdots \ge 0$ and $\lambda > 0$: if $\bar P_j \bar P_k \ge \bar P_{j+k}$ for all $j, k$, then $H$ of (2.1) is NBU.
2. First display of the proof of Theorem 5.3. If $G$ is NBU, then $\bar P_{j+k} \le \bar P_j \bar P_k$ for each damage law $F$.
3. Second display of the proof of Theorem 5.3. If submultiplicativity holds for every $F$, then $\bar G(s + j x_k) \le \bar G(s)\,\bar G(j x_k)$ for $s > 0$, $x_k = s/k$, $j = 0, 1, \dots$.

Further items (not milestones)

Theorem 5.1 (the life is exponential for every $F$ iff $G$ is exponential) and Theorem 5.2 (b), (c) (an IHR threshold makes $\bar P_k^{1/k}$ non-increasing for every $F$; non-increasing $\bar P_k^{1/k}$ for every $F$ forces $G$ to be IHRA) are posed as companion statements from the same section.

Significance

Theorem 5.3 is a characterization: the NBU class is exactly the class of threshold laws for which the cumulative-damage mechanism preserves the discrete NBU property under every damage law. Combined with Theorem 3.1 (3.5), it gives a physical derivation of NBU life distributions: an item with an NBU random strength, subject to Poisson shocks with arbitrary i.i.d. non-negative damage, has an NBU life. Theorems 5.1 and 5.2 place the exponential and the IHR/IHRA classes in the same framework, and the authors record that whether an IHRA threshold suffices in Theorem 5.2 (b) is left unresolved.

The results are proved in the paper. No machine-checked version is known to exist; this mission produces one. A complete development also supplies reusable infrastructure: convolution powers of laws on $[0, \infty)$ as Mathlib measures, Poisson mixtures of a sequence, and the ageing classes of p. 631 as predicates on survival functions.

Difficulty

The equivalence couples a property of one function, $\bar G$, to a family of inequalities indexed by every damage law, and the left side is about convolutions while the right side is pointwise. Two points make the statement harder than it looks. First, (5.1) as printed is $P\{X_1 + \cdots + X_k \le Y\}$, whereas the paper's proof works with $E\bar G(X_1 + \cdots + X_k) = P\{X_1 + \cdots + X_k < Y\}$; the two agree only when $F^{(k)}$ and $G$ have no common discontinuities, and they can disagree as soon as $F^{(k)}$ has an atom where $G$ has one, a case the left side of the equivalence includes. A formal proof cannot invoke that convention. Second, the second sentence of the theorem passes through a Poisson series (5.2) whose terms involve the whole sequence $\bar P_k$, so the NBU property of $H$ is a statement about a power series in $t$, not about any single $\bar P_k$.

Formalization scope

• A distribution is a probability measure on $\mathbb R$; "$F(z) = 0$ for $z < 0$" is mass $0$ on $(-\infty, 0)$, and "$G(0) = 0$" (Theorems 5.1, 5.2) is mass $0$ on $(-\infty, 0]$. $F^{(k)}$ is the $k$-fold Measure.conv power with $F^{(0)} = \delta_0$, and $F^{(k)}(x)$ is the mass of $(-\infty, x]$.
• $\bar P_k$ is (5.1) as printed, $\int F^{(k)}(x)\,dG(x)$ over $\mathbb R$; since $G$ is carried by $[0, \infty)$ this is $\int_0^\infty$ including an atom of $G$ at $0$, which Theorem 5.3 allows. The paper's convention that $F^{(k)}$ and $G$ have no common discontinuities is not added as a hypothesis: the statements hold for (5.1) without it. The integrand is monotone with values in $[0,1]$, so the Bochner integral is a genuine expectation.
• "For all $F$" sits inside the equivalence of Theorem 5.3 and ranges over every probability measure on $[0, \infty)$. Submultiplicativity for one fixed $F$ is a different, weaker statement.
• NBU and IHR are cross-multiplied, agreeing with the paper's ratio form wherever denominators are positive (the paper restricts variables to avoid zero denominators). NBU is on $x, t \ge 0$ exactly as in definition (v). Powers $[\bar G(t)]^{1/t}$ and $\bar P_k^{1/k}$ are real powers. "Decreasing" means non-increasing.
• $H$ is the series (2.1) as a function on $\mathbb R$, equal to $1$ on $(-\infty, 0)$; $\lambda > 0$ as in (1.1). In Theorem 3.1 (3.5) the non-negativity $\bar P_k \ge 0$ is stated explicitly.
• In Theorem 5.1 "exponential" allows rate $0$ for $H$ (the damage law $\delta_0$ gives $\bar H \equiv 1$) and requires a positive rate for $G$ ($G(0) = 0$ rules out the degenerate case $\bar G = 0$ on $(0,\infty)$).
• A trivializing formalization is ruled out: the threshold-law quantifier is not restricted to a class where both sides are automatic, the integral cannot collapse to a default value, and the NBU predicate is the paper's on $[0, \infty)$, not on $(0, \infty)$ or a vacuous domain.

Contributions welcome: proofs of the milestones, a library for Poisson mixtures and convolution powers of laws on $[0,\infty)$, and the extra items of §5.

Selected references

• J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, The Annals of Probability 1(4), 627–649, 1973. https://doi.org/10.1214/aop/1176996891
• R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965; reprinted SIAM Classics in Applied Mathematics, 1996. https://doi.org/10.1137/1.9781611971194
• Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-Out for Components and Systems, The Annals of Mathematical Statistics 37(4), 816–825, 1966. https://doi.org/10.1214/aoms/1177699362

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.

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