Markov Chain

Why accelerate value computation

Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a $\lambda$-contraction, so they converge at the geometric rate $\lambda$, the discount factor. When $\lambda$ is close to $1$, which is the regime of long effective horizons in reinforcement learning ($\lambda = 0.99$ or $0.999$) and in healthcare and operations applications, the number of iterations grows like $1/(1-\lambda)$.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that $v \mapsto v - T(v)$ behaves like the gradient of a function with smoothness constant $1+\lambda$ and strong-convexity constant $1-\lambda$. This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator $T_\pi$ of a fixed policy, they prove that both schemes converge at a rate governed by $\sqrt{\kappa}$ rather than $\kappa$, with $\kappa = (1+\lambda)/(1-\lambda)$, provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.

Setting

A finite MDP has a state set $S$ with $|S| = n$, a finite action set $A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia}$ is a probability vector), rewards $r_{ia} \in \mathbb{R}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi = (\pi_{ia})$ is a matrix with nonnegative rows summing to $1$; it induces

$$r_{\pi,i} = \sum_a \pi_{ia} r_{ia}, \qquad L_{\pi,ij} = \sum_a \pi_{ia} P_{iaj}, \qquad T_\pi(v) = r_\pi + \lambda L_\pi v .$$

The value function of $\pi$ is $v^\pi = \sum_{t \ge 0} \lambda^t L_\pi^t r_\pi$, the expected discounted reward from each starting state; it is the unique fixed point of $T_\pi$.

Reversibility (Definition 2.1): the chain with transition matrix $L$ is irreducible, and it has a stationary probability distribution $\nu$ with $\nu_i L_{ij} = \nu_j L_{ji}$ for all $i,j$.

Momentum Value Computation (M-VC) starts from arbitrary $v_0, v_1 \in \mathbb{R}^n$ and iterates

$$v_{s+1} = v_s - \alpha\,(v_s - T_\pi(v_s)) + \beta\,(v_s - v_{s-1}), \qquad s \ge 1,$$

with the constant step sizes (4.2)

$$\alpha = \frac{2}{1+\sqrt{1-\lambda^2}}, \qquad \beta = \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} .$$

The analysis runs through the $2n \times 2n$ matrix

$$B_\pi = \begin{pmatrix} \lambda(\beta+1)L_\pi & -\beta I \\ I & 0 \end{pmatrix},$$

which propagates the error of the pair $x_s = (v_s, v_{s-1})$, and its spectral radius $\rho(B_\pi)$, the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.5

For a valid MDP and a policy $\pi$ whose chain $L_\pi$ is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to $v^\pi$, and for every $\eta > 0$

$$v_s = v^\pi + o\!\left(\left(\frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} + \eta\right)^{s}\right), \qquad 0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda .$$

The goal states the paper's three clauses as printed: convergence, the little-o rate for every $\eta > 0$, and the comparison with $\lambda$.

Milestones

1. The step-size identity $\alpha = 1 + \beta$ (proof of Lemma B.1).
2. Lemma B.1: $x_s = x^\pi + B_\pi^{s-1}(x_1 - x^\pi)$ for all $s \ge 1$, with $x^\pi = (v^\pi, v^\pi)$.
3. The eigenvalues of an irreducible, reversible transition matrix are real (§2).
4. (B.1): every eigenvalue $\omega$ of $B_\pi$ satisfies $\omega^2 - \frac{2\lambda\mu}{1+\sqrt{1-\lambda^2}}\omega + \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} = 0$ for an eigenvalue $\mu$ of $L_\pi$.
5. For $\mu \in [-1,1]$, the roots $\omega^\pm(\mu)$ of (B.1) have modulus $\lambda/(1+\sqrt{1-\lambda^2})$.
6. The identity $\frac{\lambda}{1+\sqrt{1-\lambda^2}} = \frac{\sqrt{1+\lambda}-\sqrt{1-\lambda}}{\sqrt{1+\lambda}+\sqrt{1-\lambda}} = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
7. Lemma B.2: for a reversible chain, $\rho(B_\pi) = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
8. $0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda$ for $\lambda \in (0,1)$.

Significance

The rate $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$ is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number $\kappa$. Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over $\lambda$, so that an $\epsilon$-approximation of $v^\pi$ needs a number of iterations scaling like $1/\sqrt{1-\lambda}$ rather than $1/(1-\lambda)$. The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in $[-1,1]$.

The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of $B_\pi$, and the passage from spectral radius to a little-o rate.

Difficulty

The obvious argument bounds $\|B_\pi\|$ in some norm and iterates. No such bound by the rate holds in general: $B_\pi$ is not normal, and for eigenvalues $\mu = \pm 1$ of $L_\pi$ the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between $\rho(B_\pi)$ and $\|B_\pi^s\|^{1/s}$ is exactly what the $+\eta$ absorbs. Computing $\rho(B_\pi)$ needs two separate facts: the eigenvalues of $B_\pi$ are tied to those of $L_\pi$ through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of $L_\pi$ are real and lie in $[-1,1]$, which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real $\mu$ the modulus computation fails, which is why the hypothesis cannot be dropped.

Formalization scope

States and actions are finite types. The MDP data $(P, r, \lambda)$ is a plain structure, with validity (stochastic $P_{ia}$, $0 < \lambda < 1$) a separate hypothesis; the paper's initial distribution $p_0$ plays no role and is omitted. The value function is the Neumann series $\sum_t \lambda^t L_\pi^t r_\pi$. The norm on $\mathbb{R}^n$ is the sup norm, and $o(\cdot)$ is with respect to it as $s \to \infty$. Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of $B_\pi$ are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by $\nu = 0$ and is not used.

Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with $x_0 - x^\pi$, but $x_0 = (v_0, v_{-1})$ is undefined; the statement uses $x_1 = (v_1, v_0)$. Lemma B.2 prints $\rho(B_\pi) = (1-\sqrt\kappa)/(1+\sqrt\kappa)$, a negative number; its proof computes $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$, the rate of Theorem 5.5, which is stated. On p. 22 the constant $\lambda/(1+\sqrt{1-\lambda^2})$ is printed as $\lambda/(1+\sqrt{1-\lambda})^2$. The second step size, printed $\gamma$ in (4.2), is the $\beta$ of (M-VC) and App. B.

A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which $\lambda$ is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.

A complete development needs the determinant of a $2\times 2$ block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• E. Ghadimi, H. R. Feyzmahdavian, M. Johansson, Global convergence of the Heavy-ball method for convex optimization, European Control Conference, 2015. https://arxiv.org/abs/1412.7457
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 2nd ed. 2020 (cited in the paper as 2013), Chapter 6. https://doi.org/10.1007/978-3-030-45982-6
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 2014. https://doi.org/10.1002/9780470316887

Motivation

Value iteration is the standard method for solving a discounted Markov decision process (MDP), and its policy-evaluation variant, value computation (VC), computes the value of a fixed policy by iterating an affine contraction. Both converge geometrically at rate $\lambda$, the discount factor. When $\lambda$ is close to one, as in long-horizon reinforcement-learning benchmarks ($\lambda = 0.99$ or $0.999$), the number of iterations grows like $1/(1-\lambda)$, and each iteration costs a full sweep over states and actions.

In convex optimization, gradient descent on a $\mu$-strongly convex, $L$-smooth function has the same kind of rate, and Nesterov's acceleration improves the dependence on the condition number $\kappa = L/\mu$ from $\kappa$ to $\sqrt\kappa$. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read $v - T(v)$ as a gradient with "strong convexity" $1-\lambda$ and "smoothness" $1+\lambda$, transfer Nesterov's and Polyak's step sizes to value iteration, and ask when the transferred methods are actually faster. This mission covers the first answer they give: for policy evaluation on a reversible chain, the accelerated scheme converges at a rate of order $1-\sqrt{1-\lambda}$ instead of $\lambda$.

Setting

An MDP has a finite set of states $\mathbb S$ with $|\mathbb S| = n$, a finite set of actions $\mathbb A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia\cdot}$ is a probability distribution), real rewards $r_{ia}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi$ assigns to every state $i$ a probability distribution $\pi_{i\cdot}$ over actions. It induces the reward vector $r_{\pi,i} = \sum_a \pi_{ia} r_{ia}$, the transition matrix $L_{\pi,ij} = \sum_a \pi_{ia}P_{iaj}$, the policy operator $T_\pi(v) = r_\pi + \lambda L_\pi v$, and the value function

$$v^\pi = \sum_{t\ge0}\lambda^t L_\pi^t r_\pi,$$

the expected discounted reward when actions are drawn from $\pi$. VC iterates $v_{s+1} = T_\pi(v_s)$.

Accelerated Value Computation (A-VC) starts from arbitrary $v_0, v_1 \in \mathbb R^n$ and sets, for $s \ge 1$,

$$h_s = v_s + \gamma\,(v_s - v_{s-1}),\qquad v_{s+1} = h_s - \alpha\,\big(h_s - T_\pi(h_s)\big),$$

with the constant step sizes $\alpha = 1/(1+\lambda)$ and $\gamma = (1-\sqrt{1-\lambda^2})/\lambda$. Write $\kappa = (1+\lambda)/(1-\lambda)$.

A transition matrix $L$ is reversible if it is irreducible (every state reaches every other with positive probability in some number of steps) and has a stationary probability distribution $\nu$ satisfying detailed balance, $\nu_iL_{ij} = \nu_jL_{ji}$ for all $i, j$.

The analysis runs through the $2n\times2n$ matrix

$$B_\pi = \begin{bmatrix}(1-\sqrt{1/\kappa})(I+L_\pi) & -\tfrac12(1-\sqrt{1/\kappa})^2(I+L_\pi)\\ I & 0\end{bmatrix},$$

whose powers propagate the stacked error $x_s - x^\pi$, where $x_s = (v_s, v_{s-1})$ and $x^\pi = (v^\pi, v^\pi)$. Its spectral radius $\rho(B_\pi)$ is the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.1

If $L_\pi$ is irreducible and reversible, then $v_s \to v^\pi$, and for every $\eta > 0$

$$v_s = v^\pi + o\Big(\big(1-\sqrt{1/\kappa}+\eta\big)^s\Big),\qquad 0 < 1-\sqrt{1/\kappa} < \lambda.$$

The goal is stated with the $\eta$ slack because the iteration matrix has a defective leading eigenvalue: the error is of exact order $s\,(1-\sqrt{1/\kappa})^s$ in general, so a clean $O\big((1-\sqrt{1/\kappa})^s\big)$ bound is false.

Milestones

1. The step-size identities of the proof of Lemma 5.2: $1+1/\kappa-2\alpha=0$, $(1-\alpha)(1+\gamma)=\alpha\lambda(1+\gamma)=1-\sqrt{1/\kappa}$, $\alpha\gamma\lambda=(1-\alpha)\gamma=\alpha-\sqrt{1/\kappa}=\tfrac12(1-\sqrt{1/\kappa})^2$.
2. Lemma 5.2: $x_s = x^\pi + B_\pi^{s-1}(x_1-x^\pi)$ for all $s\ge1$.
3. The eigenvalues of a reversible transition matrix are real (§2, p. 4).
4. $\operatorname{Sp}(L_\pi)\subset[-1,1]$ for a reversible policy chain.
5. (5.3): each eigenvalue $\omega$ of $B_\pi$ solves $\omega^2-(\mu+1)(1-\sqrt{1/\kappa})\omega+\tfrac12(\mu+1)(1-\sqrt{1/\kappa})^2=0$ for some $\mu\in\operatorname{Sp}(L_\pi)$.
6. For $\mu\in[-1,1]$: $\tfrac12|\mu+1\pm\sqrt{\mu^2-1}|\le1$.
7. Lemma 5.3: $\rho(B_\pi) = 1-\sqrt{1/\kappa}$.
8. (5.6): $\lambda = 1-\sqrt{1/\kappa}+\sqrt{1-\lambda}\,(1-\sqrt{1-\lambda^2})/\sqrt{1+\lambda}$, with a positive last term.

Significance

The result. Since $1-\sqrt{1/\kappa} = 1-\sqrt{(1-\lambda)/(1+\lambda)}$, A-VC reaches an $\epsilon$-approximation of $v^\pi$ in $O\big((1-\lambda)^{-1/2}\log(1/(\epsilon(1-\lambda)))\big)$ iterations against $O\big((1-\lambda)^{-1}\log(1/(\epsilon(1-\lambda)))\big)$ for VC, at the same per-iteration cost. This matches the rate of Nesterov's method for strongly convex functions with the paper's identification of the constants. The same paper shows that this improvement does not extend to arbitrary MDPs: Theorem 6.3 gives a lower bound $\lambda^s/(1+\lambda)$ for every first-order method on a chain MDP, which is why reversibility (or a real spectrum, Remark 5.4) is needed here.

Formalizing it. The result is proved in the paper; no machine-checked proof exists. A formal proof needs the reality of the spectrum of reversible chains, the localization of the spectrum of a structured block matrix, and the passage from the spectral radius to a little-o rate for a matrix with a nontrivial Jordan block. The paper's printed statement puts $\eta$ under the square root, $o\big((1-\sqrt{1/\kappa+\eta})^s\big)$. That rate is faster than $\rho(B_\pi)$ and is false (a one-state chain is a counterexample). The mission poses the rate $(1-\sqrt{1/\kappa}+\eta)^s$ that the paper's own proof concludes on p. 9. This is one of four missions from this paper; the other three pose Theorem 5.5 (momentum value computation), Theorem 6.3 (the first-order lower bound) and Theorem 7.1 (safe accelerated value iteration).

Difficulty

The obvious argument says "$\rho(B_\pi)<1$, so $B_\pi^s\to0$ at rate $\rho(B_\pi)$". That argument breaks twice. First, computing $\rho(B_\pi)$ requires knowing where the eigenvalues of $L_\pi$ lie. For a general stochastic matrix they fill the unit disk, and then the roots of (5.3) can exceed $1-\sqrt{1/\kappa}$ in modulus. Reversibility is what confines them to $[-1,1]$, and the reality of the spectrum of a reversible chain is not in Mathlib. Second, the eigenvalue $1-\sqrt{1/\kappa}$ of $B_\pi$ (coming from $\mu=1$) is a double root of (5.3) with a single eigenvector, so $\|B_\pi^s\|$ is not $O(\rho^s)$; only the $\eta$-relaxed little-o holds. The eigenvalues of $B_\pi$ are non-real for $\mu\in(-1,1)$, so the whole computation must be done over $\mathbb C$.

Formalization scope

• Data. $\mathbb S$ and $\mathbb A$ are finite types. The MDP is the data $(P, r, \lambda)$. Validity (stochastic $P_{ia\cdot}$, $\lambda\in(0,1)$) and the policy property are hypotheses. Rewards are arbitrary reals. The initial-state distribution $p_0$ of the paper's tuple is omitted, since nothing here uses it.
• Reused definitions. $r_\pi$, $L_\pi$, $v^\pi$, policies and the kernel condition are the published FoundationsML.ReinforcementLearning definitions; irreducibility, stationarity and detailed balance are the published mm_basic. $v^\pi$ is the discounted reward series, not an arbitrary fixed point of $T_\pi$.
• Reversibility is irreducibility plus a stationary probability vector in detailed balance. Detailed balance alone would be satisfied by $\nu=0$ and is not used.
• Norms and rates. Vectors are functions $\mathbb S\to\mathbb R$ with the sup norm $\|\cdot\|_\infty$; "$o(\cdot)$" is Mathlib's little-o along $s\to\infty$.
• Spectra are complex: $\rho(B_\pi)$ is the spectral radius of the complexified matrix, valued in $[0,\infty]$. Using the real spectrum would make Lemma 5.3 a different, weaker statement.
• Indexing. A-VC is a sequence on $\mathbb N$ with $v_0, v_1$ given; $x_s = (v_s, v_{s-1})$ is used only for $s\ge1$.
• Pinned relative to the page. In the goal, $\eta$ is outside the square root, as in the proof. In milestone 6, $\sqrt{\mu^2-1}$ is written as $i\sqrt{1-\mu^2}$, its value for $\mu\in[-1,1]$.

Ruling out trivial readings: the hypotheses are satisfiable (a two-state chain with $P_{iaj}=1/2$ is valid, reversible and has a policy), the rate is stated with $\forall\eta>0$ rather than for some $\eta$, and $v^\pi$ is a fixed object rather than a variable constrained by hypotheses.

Needed infrastructure, reusable beyond this mission: the reality and location of the spectrum of reversible stochastic matrices (also used by the sibling mission on momentum value computation); spectra of $2\times2$ block matrices with commuting blocks; and the bound $\|M^s\| = o((\rho(M)+\eta)^s)$ from Gelfand's formula. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

• V. Goyal, J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004 (reprint 2013). https://doi.org/10.1007/978-1-4419-8853-9
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 1999 (reprint 2013), Ch. 6. https://doi.org/10.1007/978-1-4757-3124-8
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (reprint 2014). https://doi.org/10.1002/9780470316887

Payment channels and blockchain congestion

A blockchain such as Bitcoin settles a limited number of transactions per unit of time, and every on-chain transaction pays a fee that rises with congestion. The Lightning Network moves payments off the chain. Two parties lock funds in a payment channel with one on-chain transaction, and they can then pay each other any number of times by updating the channel balance privately. A new on-chain transaction is needed only when one side of the channel runs out of funds and the channel must be reset.

Guasoni, Huberman and Shikhelman (Management Science, 2023) model a channel between two nodes that pay each other at Poisson rates. They compute its cost and its optimal size, and in §3.3 they quantify how much a channel relieves the chain. The relief is the long-run number of channel transactions carried per on-chain transaction (Proposition 2). A related quantity is the probability that the payee side of the channel, not the payer side, is exhausted first (Proposition 1). This mission formalizes both results, which are statements about two finite random walks.

Setting

Node 1 commits $l_1\ge1$ units to the channel and node 2 commits $l_2\ge1$ units. Node 1 pays node 2 one unit at the jumps of a Poisson process with rate $\lambda_1$, and node 2 pays node 1 at rate $\lambda_2$, independently. Write $q=\lambda_2/\lambda_1$. The balance $X$ starts at $0$. It moves up by one when node 2 pays and down by one when node 1 pays. Node 2 has exhausted its side when $X=l_2$, and node 1 when $X=-l_1$.

Only the sequence of payments matters here, not their timing or discounting. Observed at its jumps, the balance is a random walk that steps up with probability $p=\lambda_2/(\lambda_1+\lambda_2)$ and down with probability $1-p=\lambda_1/(\lambda_1+\lambda_2)$. Two versions of this walk appear.

1. The absorbed walk on $\{-l_1,\dots,l_2\}$ stops at $-l_1$ and at $l_2$. Write $\mathbb P_0\{\tau_{l_2}<\tau_{-l_1}\}$ for the probability that, from the balance $0$, it reaches $l_2$ before $-l_1$.
2. The reset walk returns the balance to $0$ as soon as it reaches $l_2$ or $-l_1$, which models an on-chain reset of the channel. It lives on the interior balances $\{-l_1+1,\dots,l_2-1\}$. For a stationary distribution $m$ of this walk, $m(n)$ is the long-run fraction of transactions the balance spends at $n$, with $m(l_2)=m(-l_1)=0$.

The transactions that trigger an on-chain reset are the up-moves from $l_2-1$ and the down-moves from $-l_1+1$. Their stationary fraction is

$$f(m)=m(l_2-1)\,\frac{\lambda_2}{\lambda_1+\lambda_2}+m(-l_1+1)\,\frac{\lambda_1}{\lambda_1+\lambda_2},$$

and the long-term ratio of channel to on-chain transactions is $1/f(m)$.

Formalization targets

Goal: Proposition 2 (Congestion Reduction)

For $\lambda_1,\lambda_2>0$ with $\lambda_1\neq\lambda_2$ and $l_1,l_2\ge1$, the reset walk has a stationary distribution, and every stationary distribution $m$ satisfies

$$\frac1{f(m)}=\frac{(q+1)\Bigl(\bigl(l_2(q^{l_1}-1)-l_1\bigr)q^{l_2}+l_1\Bigr)}{(q-1)(q^{l_1+l_2}-1)}.$$

Milestones

• (28) and (29): $m(n)=m(0)\,\dfrac{q^{l_2}-q^n}{q^{l_2}-1}$ for $0\le n\le l_2$, and $m(n)=m(0)\,\dfrac{q^{l_1+n}-1}{q^{l_1}-1}$ for $-l_1\le n\le0$.
• (30): $m(0)=\dfrac{(q^{l_1}-1)(q^{l_2}-1)}{\bigl(l_2(q^{l_1}-1)-l_1\bigr)q^{l_2}+l_1}$.
• The on-chain fraction $f(m)$ is the reciprocal of the goal's closed form.
• Proposition 2 (i)–(ii): the closed form tends to $l_1$ as $q\downarrow0$ and to $l_1l_2$ as $q\to1$.
• Proposition 1 (i)(a),(c): $\mathbb P_0\{\tau_{l_2}<\tau_{-l_1}\}=\dfrac{1-q^{-l_1}}{1-q^{-l_1-l_2}}$ if $\lambda_2>\lambda_1>0$, and $=1$ if $\lambda_2>\lambda_1=0$.
• Proposition 1 (i)(b), corrected: for $\lambda_1=\lambda_2>0$ the probability is $l_1/(l_1+l_2)$, which is the published gambler's ruin theorem.

Significance

Proposition 2 measures how much a channel relieves the chain. A unidirectional channel of size $l_1$ carries $l_1$ payments per on-chain transaction. A symmetric bidirectional channel carries $l_1l_2$, which grows with the product of the two sizes rather than their sum. For a fixed total commitment, the relief is therefore largest when the flows are balanced. This is the paper's quantitative case that bidirectional channels reduce congestion far more than one-way ones. The probabilities of Proposition 1 tell each node how likely it is to be the one whose funds run out.

Both results are proved in the paper by elementary difference-equation arguments. Neither has a machine-checked proof. Formalizing them gives a verified closed form for the stationary law of a biased walk with resets at both ends. It also gives a biased gambler's-ruin probability on top of the platform's Markov chain library, which so far has only the fair case. The formalization also corrects case (b) of Proposition 1, which as printed claims $1/2$ for every $l_1,l_2$; the paper's own proof gives $l_1/(l_1+l_2)$.

Difficulty

The reset walk is not a birth–death chain: the balance $0$ receives the reset flow from both ends, so the walk is in general not reversible, and the detailed-balance shortcut that gives the stationary law of a reflected walk in one line fails. The balance equation (27) holds only away from $0$ and from the two reset points. In Lean, the abstract equation $mP=m$ on Fin (l₁ + l₂ - 1) must be related to recurrences indexed by integer balances, and the edge cases $l_1=1$ and $l_2=1$, where the bottom or top balance is $0$ itself, have to be handled. For Proposition 1, the hitting probability is defined as an infinite series of first-passage probabilities over trajectories, and the closed form is a statement about the value of that series.

Formalization scope

• The walks are transition matrices in the platform's MarkovMixing vocabulary (mm_basic, mm_path). Stationarity is MarkovMixing.IsStationary (nonnegative, sums to one, $mP=m$), and hitting probabilities are MarkovMixing.hitBeforeProb, a series that sums to $0$ when it is not summable. The absorbed walk is absorbed almost surely, so this convention is never triggered.
• The absorbed walk has states Fin (l₁ + l₂ + 1), with index $i$ for the balance $i-l_1$. The reset walk has states Fin (l₁ + l₂ - 1), with index $j$ for the balance $j+1-l_1$. massAt reads $m(n)$ at an integer balance and returns $0$ outside the interior, which is the paper's convention $m(l_2)=m(-l_1)=0$.
• Rates are real with $\lambda_1,\lambda_2>0$, and sizes are natural numbers $l_1,l_2\ge1$.
• The hypothesis $\lambda_1\neq\lambda_2$ ($q\neq1$) is added to Proposition 2 and to (28)–(30). The formulas divide by $q-1$, and the paper treats $q=1$ only as a limit.
• The "long-term ratio" is read as $1/f(m)$ for a stationary $m$, as in the paper's proof. Its identification with a pathwise long-run average is an ergodic theorem that the paper does not state and the mission does not ask for.
• Proposition 2 (i)–(ii) are limits of the closed form along $q\downarrow0$ and $q\to1$, $q\neq1$.
• The following would trivialize the problem and are excluded: fixing the sizes or the rates, setting $\lambda_1=\lambda_2$, defining the long-term ratio or the stationary distribution by the closed form, or quantifying over stationary distributions without proving that one exists.
• The platform has the Proved results MarkovMixing.exists_stationary_pos and MarkovMixing.stationary_unique for irreducible chains, and the fair gambler's ruin. Lemmas on stationary laws of chains with resets, and biased gambler's-ruin results on the MarkovMixing chains, would be reusable beyond this mission and are welcome.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, published online November 6, 2023, pp. 1–14. https://doi.org/10.1287/mnsc.2022.01664
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, white paper, 2016. https://lightning.network/lightning-network-paper.pdf
• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (§1.5, §2.1). https://doi.org/10.1090/mbk/058

Motivation

The two-parameter Poisson–Dirichlet distribution $\mathrm{PD}(\alpha,\theta)$ is a law on decreasing sequences $V_1 \ge V_2 \ge \cdots > 0$ with $\sum_n V_n = 1$. It describes the ranked frequencies of species in Bayesian nonparametric models (the Pitman–Yor process), the ranked lengths of excursions of Bessel processes and bridges, and the ranked cycle or block sizes in random combinatorial structures. The case $\alpha = 0$ is Kingman's one-parameter family $\mathrm{PD}(\theta)$, the law of the ranked frequencies in the Ewens sampling formula.

For $\mathrm{PD}(0,\theta)$, Vershik and Shmidt ([67]) and Ignatov ([34]) found a Markov description: the residual fractions $Y_n = V_n/(V_n + V_{n+1} + \cdots)$ form a homogeneous Markov chain, and the law is the $Y_1^\theta$-tilt of a stationary chain built from independent $\mathrm{beta}(\theta,1)$ ratios. For $\mathrm{PD}(\alpha,0)$, Proposition 8 of Pitman and Yor shows that the ratios $R_n = V_{n+1}/V_n$ themselves are independent $\mathrm{beta}(n\alpha,1)$ variables. Theorem 38 of Pitman and Yor (Ann. Probab. 25 (1997) 855–900) unifies both descriptions for the whole two-parameter family.

Timeline. Vershik and Shmidt (1977, 1978, [66, 67]) and Ignatov (1982, [34]) described the size-ordered $\mathrm{PD}(0,\theta)$ frequencies through the Markov chain $(Y_n)$; Ignatov showed that results of Vervaat and Watterson give the normalizing constant $K_{0,\theta} = \Gamma(\theta+1)e^{\theta\gamma}$ (132). Much of this was known earlier for $\theta = 1$, the case arising in combinatorics and number theory. Perman, Pitman and Yor (1992, [51]) proved the absolute continuity of $\mathrm{PD}(\alpha,\theta)$ with respect to $\mathrm{PD}(\alpha,0)$ (Proposition 14 here). Pitman and Yor (1997) announced the two-parameter Markov description as Theorem 15 and proved it as Theorem 38 for $0<\alpha<1$, quoting the case $\alpha = 0$ (Remark 40).

Setting

Fix $0 < \alpha < 1$ and $\theta > -\alpha$. The beta distribution $\mathrm{beta}(a,b)$ ($a,b>0$) has density $\frac{\Gamma(a+b)}{\Gamma(a)\Gamma(b)}x^{a-1}(1-x)^{b-1}$ on $(0,1)$. Let $\tilde Y_1, \tilde Y_2, \dots$ be independent with $\tilde Y_n \sim \mathrm{beta}(1-\alpha, \theta+n\alpha)$, and put $\tilde V_1 = \tilde Y_1$, $\tilde V_n = (1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$. The ranked values $V_1 \ge V_2 \ge \cdots$ of $(\tilde V_n)$ have, by Definition 1, the law $\mathrm{PD}(\alpha,\theta)$; $P_{\alpha,\theta}$ denotes a probability under which $(V_n)$ has this law, and $E_{\alpha,\theta}$ its expectation.

From $(V_n)$ define the ratios $R_n = V_{n+1}/V_n$ (21), the residual fractions $Y_n = V_n/(V_n+V_{n+1}+\cdots)$ (45), and $\Sigma_1 = (1-V_1)/V_1$. Conversely, from ratios define

$$Y_n = (1 + R_n + R_nR_{n+1} + \cdots)^{-1} \qquad (125).$$

The local time is $L = \lim_{n\to\infty} nV_n^\alpha$ (24).

The comparison law $P^*_{\alpha,\theta}$ makes $R_1, R_2, \dots$ independent with $R_n \sim \mathrm{beta}(\theta+n\alpha,1)$, and $Y_n$ is then defined by (125). Constants and functions:

$$K_{\alpha,\theta} = \Gamma(\theta+1)\Gamma(1-\alpha)^{\theta/\alpha}, \qquad C_{\alpha,\theta} = \frac{K_{\alpha,\theta}}{\Gamma(\theta/\alpha+1)}, \qquad \psi_\alpha(\lambda) = 1 + \alpha\int_0^1(1-e^{-\lambda x})x^{-\alpha-1}dx.$$

Formalization targets

Goal: Theorem 38 for $0<\alpha<1$

$$E_{\alpha,\theta}[f(Y_1,Y_2,\dots)] = K_{\alpha,\theta}\,E^*_{\alpha,\theta}[Y_1^\theta f(Y_1,Y_2,\dots)] \qquad (137)$$

for every nonnegative product measurable $f$; under both $P_{\alpha,\theta}$ and $P^*_{\alpha,\theta}$ the sequence $(Y_n)$ is a Markov chain with the same forward transition probabilities, with density

$$\frac{P(Y_{n+1}\in dy_{n+1}\mid Y_n = y_n)}{dy_{n+1}} = \alpha\,y_n^{-\alpha-1}(1-y_n)^{n\alpha+\theta-1}\frac{r(\alpha,\theta+n\alpha,y_{n+1})}{r(\alpha,\theta+n\alpha-\alpha,y_n)} \qquad (139)$$

on $0<y_n<1$, $0<y_{n+1}<y_n/(1-y_n)$, where $r(\alpha,\theta,y)\,dy = \Gamma(\theta/\alpha+1)y^\theta P^*_{\alpha,\theta}(Y_1\in dy) = C^{-1}_{\alpha,\theta}P_{\alpha,\theta}(V_1\in dy)$ (140); and the $P^*_{\alpha,\theta}$ law of $\Sigma_1$ is infinitely divisible with

$$E^*_{\alpha,\theta}[e^{-\lambda\Sigma_1}] = \psi_\alpha(\lambda)^{-(\theta/\alpha+1)} \qquad (141).$$

Milestones

Proposition 8 ($P_{\alpha,0} = P^*_{\alpha,0}$ on the ratios), Proposition 14 (the density $C_{\alpha,\theta}L^{\theta/\alpha}$ of $\mathrm{PD}(\alpha,\theta)$ relative to $\mathrm{PD}(\alpha,0)$), the moments (30) of $L$, the representation (143) of $L$ through the ratios, the finite-dimensional change of measure (144), its limit (145), Proposition 37 (independent ratios give a Markov chain $(Y_n)$, with co-transition density (128)), the parameter shift (146), and the conditional Laplace transform of $\Sigma_1$ given $X_1 = LV_1^{-\alpha}$.

Significance

The result. Theorem 38 reduces the size-ordered $\mathrm{PD}(\alpha,\theta)$ frequencies to a product of independent beta variables, up to a density $K_{\alpha,\theta}Y_1^\theta$ that depends on $Y_1$ alone. Any functional of the ranked frequencies can therefore be computed under a product measure. The Markov property gives the joint density of $Y_1,\dots,Y_n$ (Corollary 41), the laws of individual $V_n$ (148), and the asymptotics of $Y_n$ and $\Sigma_n$ in §7.3 of the paper. Part (iii) identifies the law of $(1-V_1)/V_1$ under $P^*_{\alpha,\theta}$, which determines the density of the largest frequency $V_1$ under $\mathrm{PD}(\alpha,\theta)$.

The formalization. The result has been proved since 1997; none of it is machine-checked. The mission formalizes the paper's own route: absolute continuity (Proposition 14), the beta product structure (Proposition 8), and a limit of finite-dimensional density ratios. It produces reusable statements about real-valued Markov chains defined through conditional laws, and about changes of measure between infinite products. Note that the printed (139) omits the factor $\alpha$; the formal statement includes it (see Formalization scope).

Difficulty

The finite-dimensional change of measure (144) is an exact computation, but its density $(R_1\cdots R_n)^\theta$ degenerates as $n\to\infty$. Passing to the limit (145) requires identifying the limit of the rescaled densities $n^{\theta/\alpha}(R_1\cdots R_n)^\theta$ with $L^{\theta/\alpha}Y_1^{-\theta}$, and an almost sure limit of densities does not by itself give the identity of expectations. A second obstacle is that the Markov property of $(Y_n)$ under $P_{\alpha,\theta}$ does not follow from any independence under $P_{\alpha,\theta}$ itself; it is transported from $P^*_{\alpha,\theta}$ through a density that is a function of $Y_1$ only, and the transported kernels must be shown to be the same. Part (iii) needs the Laplace transform of $1/V_1$ conditioned on $X_1$, which comes from the Poisson structure of $\mathrm{PD}(\alpha,0)$.

Formalization scope

Sequences are ℕ → ℝ, 0-based: V ω k is $V_{k+1}$, Yseq v k and YofR r k are $Y_{k+1}$. "$(V_n)$ has $\mathrm{PD}(\alpha,\theta)$ law" (HasPD) means that measures of preimages of measurable sets agree with those of the ranked stick-breaking map under an independent beta product (IsStickLaw); ranking counts exceedances with Set.encard. $P^*_{\alpha,\theta}$ is any probability measure on ℕ → ℝ with independent coordinates of the stated beta laws (IsStarLaw); it is defined directly as a product, never through $P_{\alpha,\theta}$. The local time $L$ is a random variable given with its defining almost sure limit (24). A Markov chain with forward kernels $\kappa_n$ (IsMarkovWith) is stated through the defining identity $E[g(Y_1..Y_n)h(Y_{n+1})] = E[g(Y_1..Y_n)\int h\,d\kappa_n(Y_n)]$; Theorem 38 (ii) asks for one family of Markov kernels serving both laws. The function $r$ of (140) is a hypothesis: any function giving the density of $Y_1$ under each $P^*_{\alpha,\theta+k\alpha}$.

Committed deviations: the goal is the case $0<\alpha<1$, the case the paper proves (the case $\alpha=0$ is quoted from [67], [34]); (139) carries the factor $\alpha$ that Bayes' rule from (128), (146) and the beta densities produces, and that Corollary 41's $\alpha^{n-1}$ confirms; (30) omits its middle expression $C^pE(\Sigma^{-\alpha p})$. Every expectation of a nonnegative quantity is a lower Lebesgue integral, so no identity can hold through the junk value of a non-integrable Bochner integral; no law is written as Measure.map of a possibly non-measurable function; no limit is taken with limUnder; and the parameter range $0<\alpha<1$, $\theta>-\alpha$ is a hypothesis of every statement that uses it.

Contributions welcome: the product-measure and beta-density computations behind (144) and (146), the limit passage (145), the Markov property of functions of independent sequences (Proposition 37), and the transfer of a Markov property through a density depending on the first coordinate.

Selected references

• J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2) (1997), 855–900. https://doi.org/10.1214/aop/1024404422
• A. M. Vershik and A. A. Shmidt, Limit measures arising in the theory of groups, I, Theory Probab. Appl. 22 (1977), 79–85; II, Theory Probab. Appl. 23 (1978), 36–49 (references [66], [67] of the paper; no link verified).
• Ts. Ignatov, On a constant arising in the theory of symmetric groups and on Poisson–Dirichlet measures, Theory Probab. Appl. 27 (1982), 136–147 (reference [34] of the paper; no link verified).
• M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92 (1992), 21–39. https://doi.org/10.1007/BF01205234

Motivation

Controlled queues are the standard testing ground for Markov decision processes with infinitely many states: the state is a queue length, which is unbounded, and the holding cost grows with it. The classical theory of the average cost criterion (Ross, Applied Probability Models with Optimization Applications, 1970) produces an optimal stationary policy only when the relative discounted values are uniformly bounded, a condition that fails for almost every queue with unbounded holding costs. Linn I. Sennott's paper Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs (Operations Research 37(4):626–633, 1989, doi:10.1287/opre.37.4.626) replaced that boundedness by one-sided conditions that are checked in practice by a monotonicity argument and a single test function. Her conditions became the standard tool for queueing control and are the basis of Chapter 7 of her book Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999).

Timeline:

• 1962–1970. Derman and Ross obtain average cost optimal stationary policies from the vanishing discount approach when the relative values $h_\alpha$ are bounded.
• 1986. Sennott treats the queue with variable service rates under bounded costs and gives a first discrete-time Tauberian argument (Operations Research 34, 1986a; 1986b).
• 1989. This paper: Assumptions 1–3, the Theorem, the Markov chain test of Propositions 4–5, and applications to a packet system and to the queue with variable service rates (Proposition 8).

Setting

A Markov decision chain has states $i=0,1,2,\dots$; in state $i$ a finite nonempty set $A_i$ of actions; a cost $0\le C(i,a)<\infty$; and transition probabilities $P_{ij}(a)$. A policy $\theta$ may depend on the whole history and may randomize; a stationary policy $f$ chooses $f(i)\in A_i$ in state $i$. For $0<\alpha<1$, $V_{\theta,\alpha}(i)$ is the expected total $\alpha$-discounted cost from $i$ and $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$, possibly infinite. The average cost of $\theta$ is

$$g_\theta(i)=\limsup_{N\to\infty}\frac1N\,E_\theta\Big[\sum_{t=0}^{N-1}C(X_t,a_t)\,\Big|\,X_0=i\Big].$$

A stationary policy $f$ is average cost optimal if there is a finite constant $g$ with $g=g_f(i)\le g_\theta(i)$ for every policy $\theta$ and every state $i$.

The queue with variable service rates (Example 2). Time is slotted; $p_i$ is the probability of $i$ arrivals in a slot, independently across slots. The state is the number of customers at the beginning of a slot. When the queue is nonempty the server chooses one of finitely many decision variables $a$ and serves at rate $a\beta\in(0,1)$, so that the customer in service leaves during the slot with probability $a\beta$; there is no decision in state $0$. From state $i\ge1$ the next state is $i-1+k$ with probability $a\beta p_k+(1-a\beta)p_{k-1}$ ($p_{-1}=0$), and from $0$ it is $j$ with probability $p_j$. The cost structure: $B(a)>0$; $Q$ a polynomial of degree $n\ge0$, nonnegative and increasing on $i\ge0$; $C(0)=Q(0)$ and $C(i,a)=Q(i)+B(a)$ for $i\ge1$. The arrival moments are $\lambda^{(k)}=\sum_i i^kp_i$ and $\lambda=\lambda^{(1)}$.

Formalization targets

Goal: Proposition 8

If $\lambda^{(n+1)}<\infty$, then

$$\lambda<\max_a(a\beta)\ \Longrightarrow\ \text{there is an average cost optimal stationary policy},$$

and

$$\lambda<\min_a(a\beta)\ \Longrightarrow\ g+h(i)=\min_a\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\quad i\ge0,$$

with $g$ the optimal average cost, $g=\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)$, and $h$ bounded below.

Milestones

1. Propositions 1–3 (p. 627): $V_\alpha$ solves the discount optimality equation, is its minimal nonnegative solution, and is the limit of value iteration (already proved on the platform, referenced).
2. The Lemma (p. 628): discount optimal stationary policies along $\alpha_n\to1$ have a stationary limit point.
3. Lemmas A1 and A2 (p. 632): the comparison between solutions of the optimality inequality and average costs, and $\limsup_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)\le g_\theta(i)$.
4. The Theorem (p. 628): under Assumptions 1–3, any limit point $f$ from the Lemma is average cost optimal, with the optimality inequalities (5); under Assumption 3*, the optimality equation (6).
5. Propositions 4, 5 and the Corollary (pp. 629–630): the Markov chain criteria that yield Assumptions 1, 3 and 3* from one well-behaved stationary policy.
6. Two steps of the proof of Proposition 8 (p. 631): $V_\alpha(i)$ is increasing in $i$ (hence Assumption 2), and the drift of $r(i)=Ai^{n+1}$ is a polynomial of degree at most $n$ with leading coefficient $A(n+1)(\lambda-a\beta)$, display (14).

Significance

Proposition 8 states that a queue in which at least one service rate exceeds the mean arrival rate has an average cost optimal stationary policy for holding costs of any polynomial growth, as long as the matching moment of the arrival distribution is finite. Bounded-cost results do not cover this case, which is the one used in practice. The general Theorem behind it is the standard vanishing discount theorem for countable-state models with unbounded costs; the Markov chain test of Propositions 4–5 and the Corollary reduces its hypotheses to a drift inequality for one policy.

All results of the paper are proved on paper. None is formalized: the platform has Sennott's discounted theory (Propositions 1–3, proved) and, as open statements, the book version of the Theorem (SennottDP.SEN.thm_7_2_3_sen_acoi), its existence part in a compact-action model (ArapostathisAC.SennottACOI.theorem_5_9), and the first half of Lemma A1 (SennottDP.SEN.lemma_7_2_1_acoi_bound). This mission states the paper's own version, with all conclusions of the Theorem, and its application to a concrete queue, which no platform item states.

Difficulty

The obvious route takes a limit of $h_\alpha=V_\alpha-V_\alpha(0)$ along a sequence $\alpha_n\to1$ and passes to the limit in the discount optimality equation. With unbounded costs and unbounded $h_\alpha$ the sum $\sum_jP_{ij}(a)h_\alpha(j)$ is an infinite series of terms that need not converge uniformly, so the limit of the sums is not the sum of the limits. Only an inequality survives (Fatou's lemma, which needs the lower bound of Assumption 2), and the equation needs the integrable upper bound of Assumption 3*. For the queue, the hypotheses are not visible from the model: they come from a monotonicity property of $V_\alpha$ and a Lyapunov drift computation whose leading term, $A(n+1)(\lambda-a\beta)i^n$, has to dominate a cost polynomial of the same degree.

Formalization scope

The model is the published Markov decision chain of Sennott (1999), SennottDP.Discounted.MDC ℕ Act, with its policies, discounted costs and value functions, and the published average cost SennottDP.SEN.avgCost; Markov chains, steady state probabilities and first passage costs are the published SennottDP.MarkovCost objects. Conventions:

• costs, discounted values and average costs lie in $[0,\infty]$; $V_\alpha$ may be infinite unless Assumption 1 is assumed;
• $h_\alpha$ is a real number, used only together with Assumption 1;
• the constants $N$ and $M_i$ of Assumptions 2–3 are explicit and chosen before $i$ and $\alpha$; Assumption 3* uses the same $M$;
• "average cost optimal" always carries a finite constant $g\ge0$ and compares with all policies, not only stationary ones;
• sums $\sum_jP_{ij}(a)h(j)$ against a real function are extended reals (positive part minus negative part);
• "ergodic" means positive recurrent (no aperiodicity);
• in the queue, every decision is formally available in state $0$ with identical cost $Q(0)$ and identical transitions, which represents "no decision in state 0"; $\lambda<\max_a(a\beta)$ is "for some $a$" and $\lambda<\min_a(a\beta)$ "for every $a$".

The second half of the goal is not "there exist $g$ and $h$ satisfying (6)": a pair solving (6) alone carries no optimality content, so the goal ties $g$ to the optimal average cost and $\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha$ and requires $h$ bounded below. The Theorem's milestones are stated for every limit point given by the Lemma, not for some stationary policy. The hypotheses of the goal are satisfiable (two-point arrivals $p_0=3/4$, $p_1=1/4$, one rate $a\beta=1/2$, $Q(i)=i+1$, $B=1$), so the goal is not vacuous.

A complete development needs a discrete Tauberian inequality (already proved on the platform), Fatou's lemma for series, a compactness argument on $\prod_iA_i$, first passage identities and a Foster–Lyapunov criterion for positive recurrence. The Markov chain criteria (Proposition 4, the Corollary) and the Theorem are reusable for every countable-state queueing control model. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• L. I. Sennott, Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs, Operations Research 37(4):626–633, 1989. https://doi.org/10.1287/opre.37.4.626
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
• S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970.
• A. G. Pakes, Some Conditions for Ergodicity and Recurrence of Markov Chains, Operations Research 17(6):1058–1061, 1969. https://doi.org/10.1287/opre.17.6.1058
• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey, SIAM J. Control Optim. 31(2):282–344, 1993. https://doi.org/10.1137/0331018