Dynamical Systems

Motivation

Learning in games asks whether players who adjust their strategies over time, by simple rules, end up at a Nash equilibrium. Many adaptive dynamics share one informational feature: each player's adjustment depends on the current play and on that player's own payoff function, but not on the payoffs of the others. Hart and Mas-Colell (AER 2003) call such dynamics uncoupled, and show that this feature alone rules out guaranteed convergence to Nash equilibrium, even for families of games in which every game has exactly one equilibrium. Earlier non-convergence results, such as Shapley's example for fictitious play and the cycling examples of Jordan (1993) and Foster and Young (1998), concern particular dynamics; this one applies to the whole class of uncoupled dynamics. It is one reason the learning literature turned to weaker targets such as correlated equilibrium, which regret-based uncoupled procedures do reach (Hart and Mas-Colell, Econometrica 2000).

The paper proves its theorem in two settings: a two-player game with a continuum of strategies (§II and the Appendix) and a three-player game with two strategies each (§III). This mission formalizes the first setting.

Setting

There are two players, $i=1,2$, and $j=3-i$ denotes the other player. Each player's strategy set is the closed unit disk $D=\{z\in\mathbb R^2:\|z\|\le1\}$, and a profile is $x=(x^1,x^2)\in X:=D\times D$. A game $\Gamma=(u^1,u^2)$ is a pair of payoff functions on $X$. A profile $\bar x$ is a (pure) Nash equilibrium if no player gains by changing only their own strategy. A dynamic for a family $\mathcal U$ of games is a vector field $F(x;\Gamma)$ on $X$ for each $\Gamma\in\mathcal U$, read $\dot x=F(x;\Gamma)$. It is uncoupled if $F^i$ depends on the game only through $u^i$: two games of $\mathcal U$ in which player $i$ has the same payoff function give the same $F^i(x;\cdot)$ at every $x\in X$.

A dynamic is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ with its Nash equilibrium $\bar x(\Gamma)$:

1. $F(\cdot\,;\Gamma)$ is $C^1$ on $X$;
2. $F(\bar x(\Gamma);\Gamma)=0$;
3. all eigenvalues of the $4\times4$ Jacobian matrix of $F(\cdot\,;\Gamma)$ at $\bar x(\Gamma)$ have negative real parts;
4. every solution $x(t)$ converges to $\bar x(\Gamma)$ as $t\to\infty$, from any initial condition.

The game $\Gamma_0$ has payoffs $u_0^i(x^i,x^j)=-\|x^i-\varphi(x^j)\|^2$. Here $\varphi:D\to D$ is continuous, $\varphi(z)=2z$ for $\|z\|\le\frac13$, $\varphi$ rotates the unit circle by $\pi/4$, and $\varphi$ is affine on rays in between. The family $\mathcal U_0$ consists of the games $u^i(x^i,x^j)=-\|x^i-\xi^i(x^j)\|^2$ with continuous $\xi^i:D\to D$ such that $\xi^i(\xi^j(x^i))=x^i$ has a unique solution. Every such game has a unique Nash equilibrium, and $\Gamma_0\in\mathcal U_0$ has the equilibrium $(0,0)$.

Formalization targets

Goal: THEOREM 1 for the game $\Gamma_0$ of §II

Let $\mathcal U$ be a family in which each game has a single Nash equilibrium and which contains every game of $\mathcal U_0$ within some $\eta>0$ of $\Gamma_0$. Then

$$F\ \text{uncoupled for}\ \mathcal U\ \Longrightarrow\ F\ \text{is not Nash-convergent for}\ \mathcal U.$$

Milestones

• the explicit $\varphi$ has the two required properties, and rotates by an angle in $[0,\pi/4]$ (fn. 21);
• every game of $\mathcal U_0$ has a unique Nash equilibrium, and that of $\Gamma_0$ is $(0,0)$;
• Lemma 2: for an uncoupled Nash-convergent dynamic on $\mathcal U_0$, at a unique best reply $F^i=0$ and the own-strategy Jacobian block $J^i$ has eigenvalues with negative real parts;
• the derivative identity, giving the Jacobian at $\Gamma_0$ the block form

$$J=\begin{bmatrix}J^1&-2J^1\\-2J^2&J^2\end{bmatrix};$$

• the coefficient $a_3=3\det(J^1)\operatorname{tr}(J^2)+3\det(J^2)\operatorname{tr}(J^1)$ of $\lambda$ in $\det(J-\lambda I)$, and Lemma 3: if $J^1,J^2$ are stable, then $J$ has an eigenvalue with positive real part;
• the main-text result: no uncoupled dynamic is Nash-convergent for $\mathcal U_0$;
• the Appendix: the functions $\psi_a$ satisfy conditions (1)–(4), and the conclusions of Lemma 2 at $\Gamma_0$ already follow from the games of $\mathcal U_0$ near $\Gamma_0$.

A companion statement, that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent, shows that the notion of Nash-convergence can be met.

Significance

The theorem identifies an informational obstruction rather than a computational one. Convergence to Nash equilibrium is easy if the dynamic may use the whole game, as the coupled dynamic $\dot x=\bar x(\Gamma)-x$ shows. It fails once each player may react only to their own payoff function, and the failure persists on an arbitrarily small neighborhood of a single game. It explains why no natural adaptive procedure has been found that converges to Nash equilibrium in general, and it motivates the stochastic, finite-memory and correlated-equilibrium variants studied afterwards (for example Hart and Mas-Colell, GEB 2006).

The result is proved in the paper. As far as the curators know, it has no machine-checked proof. A formalization fixes the model precisely. That matters here, because the conclusion depends on details the prose treats lightly: which perturbations the family must contain, what the Jacobian is at boundary points, and which solutions count.

Difficulty

The obvious argument fails because an uncoupled dynamic is a different vector field for each game, and nothing forces the fields to fit together except the uncoupledness constraint. The proof extracts information about $F(\cdot\,;\Gamma_0)$ from auxiliary games that share one player's payoff with $\Gamma_0$, and in which that player's best reply is constant. Making those auxiliary games lie in the family is the delicate part: in $\mathcal U_0$ they are immediate, but near $\Gamma_0$ they require the functions $\psi_a$ of the Appendix, whose fixed-point conditions (3) and (4) rest on an angle argument. The linear-algebra step is exact: the stability of $J^1$ and $J^2$ must be shown to force instability of the coupled $4\times4$ matrix through the sign of one coefficient of its characteristic polynomial.

Formalization scope

$\mathbb R^2$ is modelled as $\mathbb C$, and rotation by $\theta$ is multiplication by $e^{i\theta}$. Players are Fin 2, 0-based, and the other player is i + 1. A game is a pair of real functions on $\mathbb C^2$, but every definition looks only at its values on $X=D\times D$. Nash equilibria are pure equilibria in $X$ (fn. 9 notes there are no mixed ones). Derivatives are Fréchet derivatives within $X$. Eigenvalue conditions use the published predicate FatkhullinPolyak.Discrete.IsHurwitz, with the $4\times4$ Jacobian indexed in player-major order. The $C^1$ and Jacobian conditions, which the paper imposes on every dynamic it considers, are part of NashConvergent. The single-Nash-equilibrium property is a hypothesis of the goal.

Two encodings are deliberate:

• The neighborhood. "$\mathcal U$ contains a neighborhood of $\Gamma_0$" is read as the Appendix reads it: $\mathcal U$ contains every game of $\mathcal U_0$ close to $\Gamma_0$ in the sense of fn. 7. This is implied by the literal hypothesis, so the formal theorem is at least as strong. A full neighborhood contains games with several equilibria, so together with the single-equilibrium hypothesis it would make the theorem vacuous.
• Solutions. Solutions are curves that stay in $X$. If curves were allowed to leave $X$, they would follow values of $F$ that no game constrains, and Nash-convergence would fail for every $F$, which makes the goal trivial. The goal must also not be met through an empty family: the hypotheses are jointly satisfiable, for instance by $\{\Gamma\in\mathcal U_0:\Gamma\text{ within }1\text{ of }\Gamma_0\}$.

The development needs:

• calculus of $C^1$ maps on a product of disks;
• spectra of real matrices viewed over $\mathbb C$ and the characteristic polynomial of a $4\times4$ block matrix;
• elementary planar geometry of rotations and radial interpolation.

The linear-algebra milestones (block Jacobian, $a_3$, Lemma 3) are independent of game theory and reusable. Contributions are welcome on any milestone, in any order.

Selected references

• S. Hart and A. Mas-Colell, Uncoupled Dynamics Do Not Lead to Nash Equilibrium, American Economic Review 93(5), 1830–1836, 2003. https://doi.org/10.1257/000282803322655581
• S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5), 1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153
• J. S. Jordan, Three Problems in Learning Mixed-Strategy Nash Equilibria, Games and Economic Behavior 5(3), 368–386, 1993. https://doi.org/10.1006/game.1993.1022
• D. P. Foster and H. P. Young, On the Nonconvergence of Fictitious Play in Coordination Games, Games and Economic Behavior 25(1), 79–96, 1998. https://doi.org/10.1006/game.1997.0615
• S. Hart and A. Mas-Colell, Stochastic Uncoupled Dynamics and Nash Equilibrium, Games and Economic Behavior 57(2), 286–303, 2006. https://doi.org/10.1016/j.geb.2005.09.007

Motivation

Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at $n$ servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is $1/(1-\lambda)$ at load $\lambda$. With two choices it is exponentially smaller as $\lambda \to 1^-$. This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.

Timeline:

• 1994/1999. Azar, Broder, Karlin and Upfal proved the static version, balanced allocations: throwing $n$ balls into $n$ bins with $d \ge 2$ choices per ball gives a maximum load of $\log\log n/\log d + O(1)$ w.h.p., against $\Theta(\log n/\log\log n)$ for one choice (SIAM J. Comput. 1999).
• 1996. Vvedenskaya, Dobrushin and Karpelevich derived the dynamic limiting equations for $d = 2$ and showed convergence of their trajectories to the fixed point, without a rate (Problems of Information Transmission 32(1), 1996).
• 1996/2001. Mitzenmacher, independently, introduced the limiting system for general $d$, proved doubly exponential tails along every trajectory and exponential convergence to the fixed point in a weighted $L_1$ potential, and derived the limiting expected time $T_d(\lambda)$ (IEEE TPDS 2001). This mission formalizes Section 2 of that paper.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$, $0<\lambda<1$, at $n$ FIFO servers. Each customer chooses $d$ servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean $1$. Let $s_i(t)$ be the fraction of servers holding at least $i$ customers at time $t$.

A state is a sequence $s = (s_0, s_1, s_2, \dots)$ of reals with $s_0 = 1$, $s_i \ge 0$ and $s_0 \ge s_1 \ge s_2 \ge \cdots$. The empty state has $s_0 = 1$ and $s_i = 0$ for $i \ge 1$. As $n \to \infty$ the tails follow the limiting system

$$\frac{ds_i}{dt} = \lambda\,(s_{i-1}^d - s_i^d) - (s_i - s_{i+1}) \quad (i \ge 1), \qquad s_0 = 1. \tag{1}$$

A trajectory is a map $t \mapsto s(t)$, $t \ge 0$, whose values are states and whose coordinates satisfy (1) (from the right at $t = 0$). Throughout, $d \ge 2$ is an integer.

The fixed point is $\pi_i = \lambda^{(d^i - 1)/(d - 1)}$, so $\pi_0 = 1$, $\pi_1 = \lambda$, $\pi_2 = \lambda^{1+d}$. A customer arriving in state $s$ becomes the $i$-th customer of its queue with probability $s_{i-1}^d - s_i^d$ and then waits for $i$ services, so the expected time it spends in the system is

$$E(s) = \sum_{i=1}^{\infty} i\,(s_{i-1}^d - s_i^d).$$

The target constant is

$$T_d(\lambda) = \sum_{i=1}^{\infty} \lambda^{\frac{d^i - d}{d-1}}.$$

Formalization targets

Goal: Corollary 2

For $d \ge 2$ and $0 < \lambda < 1$, $T_d(\lambda) < \infty$, and:

$$\text{if } s_j(0) = 0 \text{ for some } j, \text{ then } E(s(t)) \xrightarrow[t\to\infty]{} T_d(\lambda);\qquad \text{if } s(0) \text{ is empty, then } E(s(t)) \le T_d(\lambda) \ \ \forall t \ge 0.$$

The hypothesis $s_j(0) = 0$ holds for every initial state that comes from a finite system.

Milestones, in the order the proof uses them

• Lemma 2. $\pi$ is the unique fixed point of (1) with $\sum_{i\ge1} s_i < \infty$.
• Theorem 2. If $s_j(0) = 0$ for some $j$, there are constants $N \ge 1$, $0<\alpha<1$, $\beta>1$, $\gamma>0$, independent of $t$, with $s_i(t) \le \gamma\,\alpha^{\beta^i}$ for all $i \ge N$, $t \ge 0$. From the empty state, $s_i(t) \le \pi_i$ for all $i$ and $t \ge 0$.
• Theorem 3. There are weights $w_i \ge 1$ such that $\Phi(t) = \sum_{i\ge1} w_i |s_i(t) - \pi_i|$ satisfies $\Phi(t) \le c_0 e^{-\delta t}$ ($\delta > 0$) whenever $\Phi(0) < \infty$, and in particular whenever $s_j(0) = 0$ for some $j$.
• Corollary 1. Under the conditions of Theorem 3 (weights $w_i \ge 1$ fixed before the trajectory, with $\Phi(0) < \infty$, or $s_j(0) = 0$ for some $j$), $\sum_{i\ge1} |s_i(t) - \pi_i| \le c_0 e^{-\delta t}$.
• Proof of Corollary 2, display. $\sum_{i\ge1} i(s_{i-1}^d - s_i^d) = \sum_{i\ge0} s_i^d$ for a state with $s_i \to 0$.
• Lemma 4. The drift of (1) is Lipschitz in $\ell^1$ on states, with constant $2 + 2d\lambda$.

Significance

The comparison $T_1(\lambda) = 1/(1-\lambda)$ against $T_d(\lambda)$ is the quantitative content of the power of two choices: the companion mission shows $T_d(\lambda)/\log T_1(\lambda) \to 1/\log d$ as $\lambda \to 1^-$, an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.

All results are proved in the paper (Theorem 3's proof is written out for $d = 2$ with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all $d \ge 2$, including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of $|\epsilon_i|$ in Theorem 3.

Difficulty

The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for $\ell^\infty$-bounded countable systems. The plain $L_1$ distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights $w_i$ must be built so that every coordinate's contribution to $d\Phi/dt$ is dominated by $-\delta w_i |\epsilon_i|$, while staying geometrically bounded so that $\Phi(0) < \infty$ under the doubly exponential tails of Theorem 2. Exchanging $t \to \infty$ with the infinite sum defining $E$ needs uniform tail control, which is again Theorem 2.

Formalization scope

• Namespace PowerTwoChoices.Limit; λ is lam : ℝ, $d : ℕ$ with $2 \le d$, $0 < \lambda < 1$ in every theorem.
• A state is x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every $t \ge 0$, with HasDerivWithinAt on Set.Ici 0 for each coordinate $i \ge 1$: right derivative at $t = 0$, two-sided for $t > 0$.
• Exponents are natural numbers: $\pi_i = \lambda^{\sum_{k<i} d^k}$, and $T_d$'s $i$-th term is $\lambda^{\sum_{1\le k<i} d^k}$.
• $\Phi$, the $L_1$ distance, $E$ and $T_d$ are sums in $[0,\infty]$, so a divergent series is $\infty$, never a default $0$. "Converges exponentially" (Definition 2) means $\Phi(t) \le c_0 e^{-\delta t}$ for all $t \ge 0$ with real $c_0$ and $\delta > 0$; $\delta$ may depend on the trajectory. The paper's $d(t)$ is renamed l1Dist.
• Time is real and $t \to \infty$ is Filter.atTop.
• Every theorem quantifies over trajectories; existence of a trajectory from a given state (Picard iteration, cited by the paper) is not part of the mission. The class is nonempty: the constant trajectory at $\pi$ is one.
• Ruled out: summing $E$ or $T_d$ as a real tsum (a divergent series would make the upper bound free and the limit attainable by a junk $0$), dropping the summability condition in Lemma 2 ($(1,1,\dots)$ is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for $d = 2$ only.
• Needed infrastructure: comparison principles for quasimonotone countable ODE systems, Dini-derivative Grönwall estimates, and interchange of limits and $\ell^1$ sums. All of these are reusable beyond this mission, and contributions of such lemmas as separate theorems are welcome.

Selected references

• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
• Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490
• N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing System with Selection of the Shortest of Two Queues: An Asymptotic Approach, Problems of Information Transmission 32(1), 1996, pp. 15–27.
• T. G. Kurtz, Approximation of Population Processes, SIAM, 1981. https://doi.org/10.1137/1.9781611970333

Motivation

A flexible manufacturing system processes several part types on shared machines, and a machine that switches from one part type to another pays a set-up time. Real-time, distributed scheduling rules for such systems decide locally, at each machine, when to switch and to which buffer. The simplest such rules are clearing policies: a machine keeps working on its current buffer until that buffer is empty, then switches. Perkins and Kumar (IEEE TAC 34, 1989; reference [18] of Kumar–Seidman 1990) showed that every clear-a-fraction (CAF) policy, a clearing policy that always switches to a buffer holding at least a fixed fraction of the machine's work, keeps all buffers bounded in every acyclic system whenever each machine's load is below one.

Kumar and Seidman (IEEE TAC 1990) showed that acyclicity cannot simply be dropped. In §III of the paper, a two-machine re-entrant line and a two-part-type system, both with every machine loaded below capacity, have clearing trajectories whose buffer levels grow without bound. This mission formalizes the paper's positive result for non-acyclic systems: Theorem 1, a stronger capacity condition under which every CAF policy is stable from every initial state.

Setting

There are $P$ part types and $M$ machines. Part type $p$ enters at rate $d_p>0$ and visits the machines $\mu_{p,1},\dots,\mu_{p,n_p}$ in turn; revisits are allowed. At its $i$-th stage a part waits in buffer $b_{p,i}$ and needs processing time $\tau_{p,i}>0$. Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$, and switching from $b$ to $b'\in B_m$ costs $\delta_{b,b'}\ge0$. Flows are fluid. The level $x_b(t)\ge0$ satisfies $x_b(t)=x_b(0)+u_b(t)-y_b(t)$, where $y_b$ is the cumulative output and $u_b$ the cumulative input: $d_p t$ for the first buffer of a route, the output of the previous buffer otherwise. Each machine works through runs. A run is a set-up for a buffer, during which nothing is processed, followed by processing of that buffer at rate at most $1/\tau_b$, and at exactly that rate while the buffer is nonempty.

A trajectory is clearing (Definition 1) if each machine leaves its buffer exactly at the first time the buffer is empty while another of its buffers is nonempty, and then sets up for such a buffer. It is CAF with constants $\varepsilon_m>0$, $K_m$ (Definition 2) if every set-up commenced at time $t$ is for a buffer with

$$x_{p,i}(t)\ \ge\ \varepsilon_m\sum_{(q,j):\,\mu_{q,j}=m}x_{q,j}(t)-K_m .$$

A trajectory is stable if $\sup_{t\ge0}x_{p,i}(t)<\infty$ for every buffer.

The graph on machines has an arc $m\to m'$ when $m\ne m'$ and some part type visits $m'$ right after $m$. Machines are diconnected, $m\leftrightarrow m'$, when each is reachable from the other. For each buffer, $\lambda_{p,i}$ is the last earlier stage at a different machine, if any, and $\pi_{p,i}$ is that stage's machine, the prior machine. The modified input rate is $d'_{p,i}=1/\tau_{p,\lambda_{p,i}}$ if $\pi_{p,i}\leftrightarrow\mu_{p,i}$, and $d'_{p,i}=d_p$ otherwise (11)–(13).

Formalization targets

Goal: Theorem 1 (p. 294)

If

$$\rho'_m:=\sum_{(p,i):\,\mu_{p,i}=m}d'_{p,i}\,\tau_{p,i}<1\qquad\text{for all } m, \tag{14}$$

then for all $\varepsilon>0$, all $K$, every CAF trajectory from every initial state is stable. The bound on each buffer may depend on the trajectory.

Milestones (the proof's own steps, p. 295)

For a machine $m$ in a minimal class, $V_m(t)=\sum_{\mu_{p,i}=m}x_{p,i}(t)[\tau_{p,i}+\dots+\tau_{p,i+\eta_{p,i}-1}]$ is the work at $m$ (15), and $T_n, T_{n+1}$ are consecutive set-up commencements:

1. (18): $V_m(T_{n+1})\le\max[0,V_m(T_n)-(1-\rho'_m)(T_{n+1}-T_n)+\bar\delta]$.
2. (20): $x_{p^*_n,i^*_n}(T_n)\ge 2\bar\delta/((1-\rho'_m)\tau_{p^*_n,i^*_n})\Rightarrow T_{n+1}-T_n\ge2\bar\delta/(1-\rho'_m)$.
3. $V_m(T_n)\ge\Gamma_m\Rightarrow V_m(T_{n+1})\le V_m(T_n)-\bar\delta$, with the explicit $\Gamma_m$ of p. 295.
4. Every buffer of every machine in a minimal class is bounded.
5. The induction step: with upstream classes bounded, $V_m(T_{n+1})\le\max\{\bar\Gamma,V_m(T_n)-(1-\rho'_m)(T_{n+1}-T_n)+\bar\delta+\bar\Gamma\}$.

Significance

The result. Theorem 1 is a sufficient condition for stability that holds for every system topology and every CAF policy, with no restriction to acyclic flows. It separates two kinds of upstream supply. A machine that is not in a common cycle with its supplier needs capacity only for the average rate $d_p$. A machine that is in such a cycle must budget for the supplier's peak rate. The paper's examples show that some strengthening of $\rho_m<1$ is needed for clearing policies on cyclic systems: they are unstable under $\rho_m<1$ alone. Section V of the paper builds on this gap, with a supervisory mechanism that restores stability under $\rho_m<1$ alone.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. A formalization must turn a two-page argument with a set-up/processing run structure, a starvation case analysis and an induction over the condensation of a directed graph into rigorous statements. The result is a reusable fluid model of scheduling with set-up times. It also makes explicit the conventions of the clearing rule, which the paper leaves informal.

Difficulty

A natural first attempt bounds the total work $V_m$ at each machine separately, using only the average arrival rates. This fails on cyclic systems. A machine downstream in a cycle can receive parts in bursts at the upstream machine's full processing rate $1/\tau$, far above $d_p$; Example 1 of the paper builds exactly such a positive feedback. The proof therefore has to (a) bound the inflow into a machine of a minimal class by the peak rates in (14); (b) handle starvation inside a run, where the machine works below its maximal rate; (c) control the set-up overhead, which the CAF rule amortizes by forcing long runs once $V_m$ is large; and (d) push boundedness down the partial order of classes, where the bounded upstream buffers enter as an additive constant $\bar\Gamma$. Step (d) needs a bound on the total content upstream, not one per buffer.

Formalization scope

• Model. System P M holds the data. Part types, machines and stages are 0-based (paper stage $i$ is Lean stage $i-1$). Trajectory S holds levels, cumulative outputs and runs, with N m : ℕ∞ runs per machine. Time is real, with explicit $t\ge0$. Run starts are nondecreasing and, if infinitely many, tend to infinity. Machines never idle outside runs: idling on an empty buffer is processing at the inflow rate.
• Processing law. The output is bounded by $1/\tau_b$ times the Lebesgue measure of the time spent processing $b$, with equality on intervals of processing of a nonempty buffer.
• Clearing. "Nonempty" in Definition 1 for the buffer switched to is read as nonempty or with inflow starting now. Under this reading the paper's example trajectories are clearing trajectories; read literally, "the first time" would not exist. The emptiness test on the current buffer is literal. The no-early-exit condition holds on the open processing interval.
• Set-ups. Set-ups occur only between distinct buffers. $\bar\delta$ is the largest set-up time between distinct buffers of $m$, or $0$ if there are none. Zero set-up times are allowed; $\bar\delta>0$ is not assumed.
• Constants. $\Gamma_m$, $\bar\tau$, $\underline\tau$, $\bar\Gamma$ are explicit definitions, never existentials. Every denominator is positive under the hypotheses.
• Trivializations ruled out. The trajectory class is not empty: a sorry-free witness (one machine, one buffer, $d\tau<1$, any initial level) satisfies every predicate, together with (14). The goal quantifies over every system, every $\varepsilon>0$ and $K$, and every CAF trajectory. It does not fix a selection rule, an acyclic topology, routes without revisits or positive set-ups.
• Infrastructure. Continuity of the levels (from the rate cap), restarting a trajectory at a run start, inflow bounds via conservation along routes, and the condensation of the machine graph. These are reusable for the related Kumar–Seidman missions on instability and supervisory stabilization. Proofs of the milestones in any order are welcome.

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Transactions on Automatic Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Transactions on Automatic Control 34, 139–148, February 1989 (cited as [18] in Kumar–Seidman 1990; the CAF stability result for acyclic systems).

Motivation

Products of random linear operators appear wherever a system evolves by repeated application of randomly chosen linear maps: linear recursions with random coefficients, products of random matrices in statistical physics, the growth of random dynamical systems, and population models in random environments. The basic question is the exponential growth rate of the product $Y_1Y_2\cdots Y_n$. For square matrices, Furstenberg and Kesten (Ann. Math. Statist. 31, 1960) proved that $n^{-1}\log\|Y_1\cdots Y_n\|$ converges for stationary sequences with a logarithmic moment condition.

Kingman (Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973) showed that this limit theorem is an instance of the subadditive ergodic theorem, and that the instance needs nothing of matrices beyond the norm inequality $\|AB\|\le\|A\|\,\|B\|$. His Theorem 6 therefore holds in an arbitrary real or complex Banach algebra, including infinite-dimensional ones such as infinite matrices with finite $\ell_1$ norm. It is the source of what later became known as the top Lyapunov exponent of a stationary random operator product.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. A two-parameter family is a collection $x=(x_{st})$ of random variables indexed by nonnegative integers $s<t$. Kingman's conditions (§1.1–1.2) are:

• S₁: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$;
• S₂: the joint distributions of $(x_{s+1,t+1})$ are the same as those of $(x_{st})$;
• S₃: $g_t=E(x_{0t})$ is finite for every $t\ge1$ and $g_t\ge -At$ for some constant $A$;
• S₃′: $E(x_{01}^+)<\infty$, where $x^+=\max(x,0)$.

A family of real random variables satisfying S₁, S₂ and S₃ is a subadditive process. Kingman's Theorem 1 (the goal of the first mission of this series) says that for a subadditive process $x_{0t}/t$ converges almost surely and in mean to a finite random variable $\xi$ with $E(\xi)=\gamma=\inf_{t\ge1}g_t/t$.

A Banach algebra $\mathfrak B$ is a complete normed algebra over $\mathbb R$ or $\mathbb C$ whose norm satisfies $\|AB\|\le\|A\|\,\|B\|$. A sequence $(Y_n)_{n\ge1}$ of $\mathfrak B$-valued random elements is stationary if $(Y_{n+1})_{n\ge1}$ and $(Y_n)_{n\ge1}$ have the same joint law. The log-norm process is

$$x_{st}=\log\|Y_{s+1}Y_{s+2}\cdots Y_t\|\in[-\infty,\infty),\qquad s<t,$$

with $\log 0=-\infty$. Expectations of $[-\infty,\infty)$-valued variables are extended expectations $E(f)=\int f^+\,dP-\int f^-\,dP$, defined when $\int f^+\,dP<\infty$ and possibly equal to $-\infty$.

Formalization targets

Goal: Theorem 6 (p. 893)

If $(Y_n)$ is a stationary sequence in a real or complex Banach algebra and $E\{(\log\|Y_1\|)^+\}<\infty$, then

$$\xi=\lim_{n\to\infty}n^{-1}\log\|Y_1Y_2\cdots Y_n\|$$

exists in $-\infty\le\xi<\infty$ with probability one, and

$$E(\xi)=\lim_{n\to\infty}n^{-1}E\{\log\|Y_1Y_2\cdots Y_n\|\}.$$

The goal fixes no constant and no ergodicity assumption: $\xi$ is in general a non-degenerate random variable.

Milestones

1. (1.2.7), p. 885: under S₁, S₂ and S₃′, $E(x_{st}^+)<\infty$ for all $s<t$.
2. Proof of Theorem 2, p. 886: the truncation $x^{(N)}_{st}=\max(x_{st},-N(t-s))$ is a subadditive process for every positive integer $N$.
3. Theorem 2, p. 885: if $x$ satisfies S₁, S₂ and S₃′ but not S₃, then $\xi=\lim x_{0t}/t$ exists with probability one in $[-\infty,\infty)$ and $E(\xi)=-\infty$.
4. Proof of Theorem 6, p. 893: the log-norm process satisfies S₁, S₂ and S₃′.

Significance

Theorem 6 defines a stochastic spectral radius: if every $Y_n$ equals a fixed element $y$, then $e^\xi$ is the spectral radius of $y$ by Gelfand's formula, and for independent $Y_n$ with common law $\pi$ the limit is a constant $\rho(\pi)$ depending only on $\pi$. For $k\times k$ matrices the theorem reduces to the Furstenberg–Kesten theorem. Theorem 2, the extension of the subadditive ergodic theorem from S₃ to S₃′, is the form needed whenever a process can have mean growth rate $-\infty$, as happens for products that can vanish or contract superlinearly; it is used well beyond random products.

All results here are proved on paper (Kingman 1973, building on his 1968 paper). None of them is machine-checked: Mathlib has no subadditive ergodic theorem, no Furstenberg–Kesten theorem and no random-product limit in normed algebras. The platform poses an ergodic, constant-limit form of Kingman's theorem (PalmQueueing.Ergodic.kingman_subadditive, open); this mission's Theorem 2 is a different statement (non-ergodic, conclusion $E(\xi)=-\infty$ under failure of S₃). A complete development would give the first formal proof of the Furstenberg–Kesten limit, in the generality of Banach algebras.

Difficulty

Theorem 6 is short given Theorems 1 and 2, but the obvious one-line reduction to Theorem 1 fails in two places. First, the log-norm process can take the value $-\infty$ and its means $g_t$ can be $-\infty$ or decrease superlinearly, so condition S₃ fails and Theorem 1 does not apply; the case $E(\xi)=-\infty$ is a separate theorem (Theorem 2), whose proof must exchange a limit in $t$ with a limit in an auxiliary parameter. Second, stationarity of the log-norm process (S₂) is a statement about joint laws on a path space; in a non-separable Banach algebra, multiplication need not be measurable for the product $\sigma$-algebra on $\mathfrak B\times\mathfrak B$, so it is not automatic that the law of $(Y_n)$ determines the joint law of the products $Y_{s+1}\cdots Y_t$. The main dependency, Theorem 1 itself, is the subject of a separate mission and is not restated here.

Formalization scope

The Lean development fixes these conventions:

• Families are functions x : ℕ → ℕ → Ω → β; only pairs $s<t$ enter any condition. S₁ is required almost surely for each triple (the weaker hypothesis); the log-norm milestone proves it at every sample point.
• S₂ and stationarity are equalities of laws of the whole path (Measure.map) on the product $\sigma$-algebra, not equality of one-dimensional marginals.
• S₃′ and all positive parts are lower Lebesgue integrals; expectations that may be $-\infty$ are computed as $\int f^+ - \int f^-$ in EReal, never as Bochner integrals (which return $0$ for non-integrable functions).
• $\log\|\cdot\|$ is ENNReal.log of the norm, so $\log\|0\|=-\infty$; Real.log 0 = 0 would replace a vanishing product's growth rate $-\infty$ by $0$, and is ruled out.
• $\mathfrak B$ is a complete unital NormedRing with NormedAlgebra 𝕜 𝔅, RCLike 𝕜. Each $Y_n$ is strongly measurable; $\mathfrak B$ is not assumed separable.
• Limits are Filter.atTop on ℕ in the topology of EReal; the conclusions assert $\xi<\infty$ almost surely, $E(\xi^+)<\infty$, and, for (2.3.5), both the existence of the limit of means and its value.

A formalization that replaces the extended logarithm by Real.log, or the extended expectation by a Bochner integral, makes the statement false or trivially different, and is excluded.

Reusable infrastructure: extended expectations of EReal-valued random variables, joint-law stationarity of sequences and two-parameter families, and the truncation lemma for S₃′ processes. Contributions toward Theorem 1 (mission 1 of this series), toward measurability of products of strongly measurable random elements, and toward the milestones in any order are welcome.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
• J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30:499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x
• H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31:457–469, 1960. https://doi.org/10.1214/aoms/1177705909

Products of random matrices

Many systems evolve by repeated multiplication by a random linear map: the state of a linear system with randomly varying coefficients, population vectors in a random environment (Leslie models whose rates change from year to year), the transfer matrices of a disordered one-dimensional medium, and the transition operators of a Markov chain in a random environment. In each case the object of interest is the product $X_n = Y_1 Y_2 \cdots Y_n$ of random matrices and its growth as $n\to\infty$.

The basic answer is due to Furstenberg and Kesten (Products of random matrices, Ann. Math. Statist. 31 (1960)): under a logarithmic moment condition and stationarity, $n^{-1}\log$ of the size of $X_n$ converges. Their proof was a substantial piece of analysis. In his 1973 IMS Special Invited Paper (Kingman, Subadditive ergodic theory, Ann. Probab. 1 (1973)), J. F. C. Kingman showed that for matrices with strictly positive entries the result is a short corollary of his subadditive ergodic theorem (Theorem 1 of that paper, 1968). This mission formalizes that application: Theorem 5 of the 1973 paper, §2.2, pp. 891–892.

Timeline:

• 1960: Furstenberg and Kesten prove convergence of $n^{-1}\log\|X_n\|$ and, for positive matrices, of $n^{-1}\log[X_n]_{ij}$.
• 1968: Kingman proves the subadditive ergodic theorem (J. Roy. Statist. Soc. B 30).
• 1973: Kingman's survey deduces the positive-matrix theorem (Theorem 5) and the general Banach-algebra version (Theorem 6) from it.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $k\ge1$, and let $Y_1, Y_2,\dots$ be random $k\times k$ real matrices. Write $[A]_{ij}$ for the $(i,j)$th entry of a matrix $A$, and

$$X_n = Y_1 Y_2\cdots Y_n \qquad (2.2.1),$$

the product taken left to right. The sequence $(Y_n)$ is stationary if the joint law of $(Y_2, Y_3, \dots)$ equals the joint law of $(Y_1, Y_2, \dots)$; this is a statement about all finite-dimensional distributions at once, and it includes the case of independent identically distributed matrices.

The proof works with the diagonal process

$$z_{st} = [Y_{s+1}Y_{s+2}\cdots Y_t]_{11},\qquad x_{st} = -\log z_{st}\qquad (s<t),$$

and with the $\ell_1$-norm $\|A\| = \max_i \sum_j |[A]_{ij}|$. A family $(x_{st})_{s<t}$ is a subadditive process (§1.1) if S₁: $x_{su}\le x_{st}+x_{tu}$ for $s<t<u$; S₂: the joint distributions of $(x_{s+1,t+1})$ equal those of $(x_{st})$; S₃: $g_t=E(x_{0t})$ exists and $g_t\ge -At$ for some constant $A$.

Formalization targets

Goal: Theorem 5

Suppose the elements of the matrices $Y_n$ are strictly positive, $E|\log[Y_n]_{ij}|<\infty$ for every $n$ and every $i,j$, and $(Y_n)$ is stationary. Then there is one finite random variable $\lambda$ such that for every $(i,j)$

$$\lambda = \lim_{n\to\infty} n^{-1}\log [X_n]_{ij} \qquad (2.2.2)$$

with probability one and in mean. The limit is random in general (it is constant when $(Y_n)$ is ergodic); the theorem asserts its existence, its finiteness and its independence of $(i,j)$, and nothing about its value.

Milestones, in the order of the paper's proof

1. (2.3.1): $[AB]_{11}\ge[A]_{11}[B]_{11}$ for matrices with strictly positive entries.
2. $x_{st}=-\log z_{st}$ satisfies S₁ and S₂, and each $x_{st}$ has finite expectation $g_{t-s}$.
3. $E\{\log\|Y_1\|\}<\infty$ and $g_n/n\ge -E\{\log\|Y_1\|\}$ for all $n\ge1$, so S₃ holds.
4. The limit (2.2.2) exists, with probability one and in mean, for $i=j=1$.
5. (2.2.3): for every $(i,j)$, $P\{\liminf n^{-1}\log[X_n]_{ij}\ge\lambda\}=1$.
6. For every $(i,j)$, $P\{\limsup n^{-1}\log[X_n]_{ij}\le\lambda\}=1$.

Significance

The limit $\lambda$ is the top Lyapunov exponent of the random product: it is the almost-sure exponential growth rate of every entry, and hence of every norm, of $X_n$. It governs the stability of random linear recursions $v_{n}=v_{n-1}Y_n$, the long-run growth rate of populations in random environments, and localization in one-dimensional disordered systems. Theorem 5 is the existence statement on which all of these quantitative questions rest.

The theorem has been proved since 1960, and Kingman's derivation is a classical model application of subadditive ergodic theory. To our knowledge it has no machine-checked proof: Mathlib has neither Kingman's subadditive ergodic theorem nor any limit theorem for random matrix products. This mission produces a formal statement of the result together with the formal decomposition of the proof into the steps Kingman writes down; its milestone 4 is exactly where the subadditive ergodic theorem (the goal of the companion mission Subadditive Ergodic Theory 1) is applied.

Difficulty

Milestones 1–3 are deterministic matrix inequalities plus integrability bookkeeping; the substance is elsewhere. First, milestone 4 needs the full subadditive ergodic theorem, almost-sure and in mean, for a non-ergodic stationary process: the classical Birkhoff theorem does not apply, because $\log[X_n]_{11}$ is not a sum of stationary increments. Second, passing from the diagonal entry to all entries requires controlling $n^{-1}\log[Y_n]_{1j}$ along a stationary sequence with only a first-moment hypothesis, and transporting an almost-sure statement about $X_n'=Y_2\cdots Y_{n+1}$ back to $X_n$ by stationarity, where the limit $\lambda$ is itself random. The natural shortcut — treating $\lambda$ as a constant — is only valid under ergodicity, which is not assumed.

Formalization scope

• Matrices are Matrix (Fin k) (Fin k) ℝ with NeZero k; the paper's index $1$ is 0 : Fin k. The sequence is Y : ℕ → Ω → Matrix …, read only for $n\ge1$; Y 0 plays no role.
• Products are ordered: $Y_{s+1}\cdots Y_t$ is the List.prod of [Y (s+1), …, Y t]; $X_0$ is the identity.
• Stationarity is equality of the laws of $(Y_{n+2})_{n\ge0}$ and $(Y_{n+1})_{n\ge0}$ on ℕ → Fin k → Fin k → ℝ with the product σ-algebra. Independence is not assumed.
• Positivity holds for every outcome; "their logarithms have finite expectations" is integrability of every $\log[Y_n]_{ij}$, $n\ge1$.
• "Finite limit" is a real-valued lam : Ω → ℝ; "in mean" is $E|n^{-1}\log[X_n]_{ij}-\lambda|\to0$ with $\lambda$ integrable; time is $n\in\mathbb N$ with Filter.atTop. One lam serves all $(i,j)$.
• Lim inf and lim sup inequalities are stated with $\varepsilon$: almost surely, for every $\varepsilon>0$, eventually $n^{-1}\log[X_n]_{ij}\ge\lambda-\varepsilon$ (respectively $\le\lambda+\varepsilon$), which avoids the junk value of a real liminf on unbounded sequences.
• Real.log 0 = 0 in Lean; the statements apply log only to entries that are strictly positive under the hypotheses, so no junk value enters. Dropping the positivity hypothesis would change the theorem, and is not an acceptable shortcut.
• The S₁/S₂ vocabulary of §1.1 comes from the group's shared process module; this mission defines $g_t$ locally. The general subadditive ergodic theorem is not restated here, and milestone 4 is the object-specific statement the paper writes.

Welcome contributions: proofs of the matrix inequalities, the integrability and stationarity transfer lemmas, a formal subadditive ergodic theorem (shared with the companion mission).

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
• H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31(2):457–469, 1960. https://doi.org/10.1214/aoms/1177705909
• J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

Motivation

Many random growth models attach a cost, distance, or accumulated quantity to each time interval. If the quantity over a long interval is at most the sum over two adjacent intervals, it is subadditive. A stable rate over long intervals is useful even when the underlying random system does not have a simple independent-increment description. Kingman's 1973 account places percolation and products of random matrices among the applications of this framework. Its basic theorem treats integer time; the present mission concerns the change to every nonnegative real time. Kingman, §1.1 and §1.4.

The change matters because observing a process at integer times can miss arbitrarily large behavior between observations. Kingman gives a smooth stationary-increment example in Theorem 3 where no prescribed increasing bound eventually controls the values at all real times. Theorem 4 gives a condition that does control this local behavior. These two results together explain why the continuous-time statement needs more than a formal change of index type. Kingman, Theorems 3–4.

Setting

Work on a probability space $(S,\mathcal F,P)$. A continuous-parameter subadditive process is a family of real random variables $x_{st}$ indexed by $0\le s<t$. It satisfies $x_{su}\le x_{st}+x_{tu}$ whenever $0\le s<t<u$. Its stationarity says that, for every real shift $\tau\ge0$, the complete shifted family $(x_{s+\tau,t+\tau})_{s<t}$ has the same joint distribution as $(x_{st})_{s<t}$. Finally, the mean $g_t=E(x_{0t})$ exists as a finite real number for each $t>0$ and obeys $g_t\ge-At$ for one constant $A$. These are the continuous-time versions of Kingman's conditions S₁, S₂, and S₃. Equality of the law of each individual coordinate would be too weak for S₂. Kingman, pp. 883–884, 887.

For an interval $I\subseteq[0,\infty)$, the oscillation is $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$. A process has the local oscillation condition when $E(\Omega_I)<\infty$ for one nondegenerate interval $I$. In §1.4 the paper states that this condition then holds on every bounded interval. The quantity $\gamma=\inf_{t>0}g_t/t$ is the mean growth rate. Kingman, (1.4.1), (1.4.6)–(1.4.7).

The paper also requires separability. Here this means that, outside one probability-zero set, the value at every admissible pair of times can be approached along a sequence from a fixed countable dense set of pairs. It is a condition on how the uncountable family is observed, and it permits discontinuous sample paths. Kingman cites the standard separability convention without defining it in §1.4; the mission makes the convention explicit. Kingman, Theorem 4 and following discussion.

Formalization targets

Theorem 4: convergence at all real times

For a separable process satisfying S₁–S₃ and the local oscillation condition, the target is an integrable real random variable $\xi$ such that

$$\frac{x_{0t}}{t}\longrightarrow\xi\quad\text{almost surely and in }L^1(P) \quad(t\to\infty,\ t\in\mathbb R), \qquad E(\xi)=\gamma=\inf_{u>0}\frac{g_u}{u}.$$

The time variable ranges over all real values tending to infinity. The integer-time assertion (1.4.8) is a separate milestone, not the goal. Other milestones identify the deterministic mean rate, extend the oscillation condition to bounded intervals, record the bounds at times between consecutive integers, and state the vanishing of normalized unit-interval oscillation. Each comes from a sentence or display in §1.4. Kingman, Theorem 4 and proof.

Significance

Theorem 4 gives a long-run rate for a broad stationary subadditive family without assuming that its trajectories are continuous or differentiable. Its mean statement identifies the expectation of the random limit with a deterministic infimum of normalized expectations. The paper notes that the usual continuous-time ergodic theorem for additive integral processes is a corollary, because such processes satisfy its oscillation condition. The condition is therefore compatible with familiar additive models while also covering discontinuous subadditive ones. Kingman, p. 890.

The theorem and its argument are known from the paper; this mission asks for a machine-checked development of the stated result. A completed development would provide reusable formal interfaces for joint-law stationarity of an uncountable family, separability, extended-valued oscillations, and almost-sure plus $L^1$ limits. The proposed theorem statements compile as open goals; compiling them does not prove them. Kingman, §1.4.

Difficulty

An integer-time subadditive theorem controls $x_{0n}/n$ only on its discrete skeleton. It cannot by itself rule out large values of $x_{0t}/t$ for times between consecutive integers; Theorem 3 shows that such behavior can occur even with smooth stationary sample paths and finite expectations. A continuous-time result must control local variation as the observation window moves to large times. The uncountable supremum in $\Omega_I$ also needs a genuine extended value and a measurability convention. Kingman, Theorems 3–4.

The paper's displayed assertion (1.4.1), that $g_t/t$ converges as real $t\to\infty$ under S₁–S₃ alone, needs qualification: a discontinuous additive function can make a deterministic subadditive mean with no such limit. The corresponding milestone includes the finite-oscillation condition assumed by Theorem 4. This correction is disclosed in the theorem's formalization note. Kingman, (1.4.1), (1.4.7).

Formalization scope

Lean indexes the family by $\mathbb R\to\mathbb R\to S\to\mathbb R$ and uses only $0\le s<t$; values at other pairs carry no meaning. Each valid coordinate is measurable. S₁ is pointwise in the sample point, while S₂ is equality of the probability laws of the complete path before and after every nonnegative real shift. S₃ states integrability of $x_{0t}$ for every $t>0$ and one linear lower bound on its mean. The sample-space type is called $S$ so that $\Omega_I$ denotes oscillation without ambiguity.

Oscillation is valued in the extended nonnegative reals. Thus an unbounded supremum is infinite, and the expected-oscillation condition cannot hold because of a default real-supremum value. Separability is the countable graph-approximation condition outside one measurable null set. The premise is finiteness on one closed interval $[a,b]$ with $0\le a<b$; the propagation milestone covers bounded intervals with either choice of endpoints. The limit in Theorem 4 uses the filter at infinity on real time. Its almost-sure convergence and convergence in mean are separate clauses, and $\xi$ is integrable. No continuity of paths, ergodicity, or independence is assumed.

A complete proof may build on Mathlib's measure theory, filters, Borel–Cantelli lemmas, and real analysis. The process and oscillation definitions, along with the finite-oscillation and skeleton statements, are reusable beyond this particular theorem. Contributions that establish these interfaces and the named intermediate statements are within scope. A statement limited to integer times, a marginal-only version of stationarity, or a real supremum that returns a default value on an unbounded set would not express this target.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. DOI: 10.1214/aop/1176996798.

Motivation

A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).

The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.

Setting

There are $K$ classes, numbered in route order, and $I$ stations. Every unit of fluid enters class $1$ at rate one. On completing service in class $k$, it becomes class $k+1$; after class $K$, it leaves. The station serving class $k$ is $\sigma(k)$. Different classes may share a station. The constituency of station $i$ is $C_i=\{k:\sigma(k)=i\}$, and class $k$ has positive mean service requirement $m_k$, so its service rate is $\mu_k=1/m_k$. The nominal workload at station $i$ is $\rho_i=\sum_{k\in C_i}m_k$. The paper assumes $\rho_i<1$ at every station. Dai and Weiss (1996), pp. 115–117.

For time $t\ge0$, $Q_k(t)$ is the amount of fluid in class $k$, and $T_k(t)$ is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each $Q_k$ remains nonnegative, each $T_k$ starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.

A priority ranking $\pi$ assigns a distinct rank to every class, with smaller rank meaning higher priority. For class $k$, let $H_k$ contain the classes at the same station whose rank is at least as high as $k$'s. In a preemptive-resume priority fluid model, capacity unused by $H_k$ may increase only when the fluid workload in $H_k$ is zero. Under LBFS, $\pi(k)=K+1-k$: a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.

Formalization targets

Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and $\rho_i<1$:

$$\exists\delta>0\;\forall (Q,T),\quad \bigl[(Q,T)\text{ is an LBFS fluid solution and }|Q(0)|=1\bigr] \Longrightarrow \forall t\ge\delta,\;Q(t)=0,$$

where $|Q(0)|=\sum_{k=1}^K Q_k(0)$. The same $\delta$ must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.

The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time

$$\delta=\frac{|Q(0)|}{\widehat\lambda-1},\qquad \widehat\lambda=\frac{1}{\max_{1\le i\le I}\rho_i}>1.$$

The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.

Significance

The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.

Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.

Difficulty

The load inequalities $\rho_i<1$ compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.

Formalization scope

Lean represents classes and stations by finite index types. Their indices start at zero: Lean class $k-1$ corresponds to paper class $k$, and LBFS is Fin.revPerm. The paths $Q$ and $T$ are functions on all real times, while the fluid equations and conclusions are imposed only for $t\ge0$. The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.

The service requirements $m_k>0$ are explicit so $\mu_k=1/m_k$ has its intended value. The drift and emptying-time milestones explicitly assume $K>0$, since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when $K=0$, its normalization $|Q(0)|=1$ is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. DOI: 10.1287/moor.21.1.115.

Why priority rules in reentrant lines matter

Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.

Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.

Timeline:

• 1991. Lu and Kumar exhibit a two-station reentrant line that is unstable under a static priority rule with every workload below one.
• 1993. Kumar proves stability of FBFS and LBFS for discrete deterministic reentrant lines.
• 1995. Dai shows that stability of the fluid model implies positive Harris recurrence of the stochastic network.
• 1996. Dai and Weiss prove that the FBFS and LBFS fluid models of every reentrant line are stable (Theorems 4.3 and 4.4), and with Dai's theorem obtain stability of the stochastic networks.

Setting

A reentrant line has $I$ stations and $K$ classes. All fluid follows one route: it enters as class $1$, becomes class $k+1$ when class $k$ is completed, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$, and $\mu_k = 1/m_k$. The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$, and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$. The exogenous arrival rate is $1$. The standing assumption of the paper is

$$\rho_i < 1 \qquad (i = 1,\dots,I). \tag{1.7}$$

A fluid model solution is a pair of paths $Q(t) = (Q_k(t))_k$, the fluid levels, and $T(t) = (T_k(t))_k$, the cumulative service time given to each class, such that for $t \ge 0$:

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t), \qquad Q_k(t) \ge 0,$$

with $\mu_0T_0(t) = t$; each $T_k$ starts at $0$ and is nondecreasing; and the idle time $U_i(t) = t - \sum_{k\in C_i}T_k(t)$ of each station is nondecreasing.

A buffer priority discipline is a permutation $\pi$ of the classes; a class $k$ has priority over a class $l$ at the same station when $\pi(k) < \pi(l)$. Write $H_k = \{l \in C_{\sigma(k)} : \pi(l) \le \pi(k)\}$, $T_k^+ = \sum_{l\in H_k}T_l$, $U_k^+(t) = t - T_k^+(t)$ and $W_k^+ = \sum_{l\in H_k} m_l Q_l$. Under preemptive resume, $U_k^+$ may increase only at times when $W_k^+ = 0$ (condition (4.4)): a station never idles toward the classes of priority at least that of $k$ while any of them holds fluid. FBFS is $\pi(k) = k$, so earlier steps of the route have priority.

The fluid model is stable (Definition 1.3) if there is a time $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$.

Formalization targets

Goal: Theorem 4.3

For every reentrant line with $m_k > 0$ and (1.7),

$$\text{the fluid model (1.8)–(1.12), (4.4) with } \pi(k) = k \text{ is stable.}$$

The goal asserts existence of an emptying time; it does not fix the value.

Milestones

1. Lemma 2.2 (i): a nonnegative function has zero derivative wherever it vanishes and is differentiable.
2. Lemma 2.2 (ii): an absolutely continuous nonnegative $g$ whose derivative is at most $-\varepsilon$ wherever $g > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
3. Proposition 4.2: at a regular time of a priority fluid model, an empty buffer has equal in- and out-flow rates, and at each station the highest-priority nonempty class satisfies $\sum_{k\in H_{k_0}} m_kd_k = 1$ while lower-priority classes have zero out-flow.
4. Inductive step (proof of Theorem 4.3): once buffers $1,\dots,k-1$ stay empty from $t_{k-1}$ on, buffer $k$ is empty from $t_k = t_{k-1} + Q_k(t_{k-1})m_k/(1 - \sum_{l\in H_k} m_l)$ on.
5. Emptying time (proof of Theorem 4.3): every solution with $|Q(0)| = 1$ is empty from

$$\delta = \sum_{k=1}^K m_k\frac{\prod_{l=1}^{k-1}(1-\sum_{j\in H_l\setminus\{l\}}m_j)}{\prod_{l=1}^{k}(1-\sum_{j\in H_l}m_j)}$$

on, which gives the goal with an explicit constant.

Significance

Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.

Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.

Difficulty

The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer $k-1$ is empty" is not enough. Finally, the explicit constant $\delta$ requires bounding the content of buffer $k$ at time $t_{k-1}$ by the total content, which may have grown since time $0$.

Formalization scope

• Classes and stations are Fin K and Fin I, 0-based: the paper's class $k$ is Lean index $k-1$.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed on $t \ge 0$ only, and derivatives are taken at $t > 0$.
• Conditions (1.13) and (4.4) are in interval form (ConstantWhile): the idle process is constant on every interval of $[0,\infty)$ on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.
• Lipschitz continuity of the paths is not assumed; it follows from the monotonicity conditions.
• $m_k > 0$ is an explicit hypothesis; the paper takes it for granted.
• Priorities are Equiv.Perm (Fin K), FBFS is the identity; $|Q(0)|$ is $\sum_k Q_k(0)$.
• In Lemma 2.2 (ii) the printed strict "$\dot g(t) < -\varepsilon$" is relaxed to "$\le -\varepsilon$", as every application requires; absolute continuity is dropped from Lemma 2.2 (i), where it is not needed. Both changes strengthen the lemma.
• In the inductive step, "stay empty for $t > t_{k-1}$" is read as $t \ge t_{k-1}$, and the case $Q_k(t_{k-1}) = 0$ is included.
• The stochastic network is not formalized; only the fluid model is.

A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with $|Q(0)| = 1$, so stability is not vacuous.

Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1) (1996) 115–134. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1) (1995) 49–77. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13 (1993) 87–110. https://doi.org/10.1007/BF01149327
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12) (1991) 1406–1416. https://doi.org/10.1109/9.106159