Dynamical Systems

Motivation

Planar flows are tame: the Poincaré–Bendixson theorem says that a bounded forward orbit in the plane tends to a fixed point or a periodic orbit. From dimension three on this fails, and the long-time behavior of a flow has to be described through sets rather than single orbits. Chapter 8 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (AMS GSM 140, 2012; author's preliminary version at mat.univie.ac.at) develops two tools for this. The first is the attracting set produced by a trapping region, the device used to show that the Lorenz equation (Lorenz 1963) has an attractor. The second is volume: Liouville's formula for volumes measures how a flow expands or contracts phase space, which shows that the Lorenz attractor has Lebesgue measure zero, and in the special case of a Hamiltonian system gives Liouville's theorem, that the flow preserves volume. Liouville's theorem, with Poincaré's recurrence theorem as its companion, underlies Hamiltonian mechanics and equilibrium statistical mechanics.

This mission states those results for the local flow of a $C^1$ vector field on an open subset of $\mathbb{R}^n$, as in the book.

Setting

Let $M \subseteq \mathbb{R}^n$ be open and $f : M \to \mathbb{R}^n$ of class $C^1$. An integral curve of $\dot x = f(x)$ is a differentiable $\varphi$ on an open interval with $\dot\varphi(t) = f(\varphi(t))$. For each $x \in M$ there is a unique maximal one through $x$ at time $0$, defined on the open interval $I_x \ni 0$. Its value at time $t$ is $\Phi(t, x)$, the flow. The flow is local: $I_x$ may be bounded.

For $X \subseteq M$, the $\omega_+$-limit set $\omega_+(X)$ is the set of $y \in M$ for which there are $t_k \to \infty$ and $x_k \in X$ with $\Phi(t_k, x_k) \to y$. The stable and unstable sets of $\Lambda$ are $W^\pm(\Lambda) = \{x \in M : d(\Phi(t, x), \Lambda) \to 0 \text{ as } t \to \pm\infty\}$, where $d$ is the distance to a set. A set is invariant if it contains the full orbit of each of its points. An invariant $\Lambda$ is attracting if $W^+(\Lambda)$ is a neighborhood of $\Lambda$. A trapping region is an open connected $E$ with compact closure $\overline E \subseteq M$ such that $\Phi(t, \overline E) \subset E$ for all $t > 0$.

The divergence of $f$ is $\operatorname{div} f = \sum_i \partial f_i / \partial x_i = \operatorname{tr}(df)$. On phase space $\mathbb{R}^n \times \mathbb{R}^n \ni (p, q)$, a Hamilton function $H \in C^2$ defines Hamilton's equations $\dot q = \partial H / \partial p$, $\dot p = -\partial H / \partial q$, whose right-hand side is the Hamiltonian vector field $X_H$. The Lorenz equation is $\dot x = -\sigma(x - y)$, $\dot y = rx - y - xz$, $\dot z = xy - bz$ with $\sigma, r, b > 0$. Volume $|\cdot|$ is Lebesgue measure.

Formalization targets

Goal: Liouville's theorem (Theorem 8.10)

For $H \in C^2(\Omega)$ on an open $\Omega \subseteq \mathbb{R}^n \times \mathbb{R}^n$, with $\Phi$ the flow of $X_H$ on $\Omega$, every measurable $U \subseteq \Omega$ and every time $t$ at which all points of $U$ are alive satisfy

$$|\Phi(t, U)| = |U| .$$

Milestones

• Lemma 8.8 (Liouville's formula for volumes). Take $f \in C^1(\mathbb{R}^n)$, $U$ bounded and open, and $t_0$ with every point of $\overline U$ alive at $t_0$. Write $V(t) = |\Phi(t, U)|$. Then $V(t_0) < \infty$ and

$$\dot V(t_0) = \int_{\Phi(t_0, U)} \operatorname{div} f(x)\,dx .$$

• Theorem 8.11 (Poincaré). Let $\Phi$ be a volume preserving bijection of a bounded region $D$. Then every neighborhood $U \subseteq D$ contains an $x$ with $\Phi^k(x) \in U$ for some $k \ge 1$.
• Lemma 8.5. For a trapping region $E$, $\Lambda = \omega_+(E) = \bigcap_{t \ge 0} \Phi(t, E)$ is nonempty, invariant, compact, connected and attracting.
• Lemma 8.6. For a trapping region $E$, $W^-(x) \subseteq \omega_+(E)$ for every $x \in \omega_+(E)$.
• Lemma 8.7. For the Lorenz equation with $r \le 1$, the origin is the only fixed point, and every solution exists for all $t \ge 0$ and tends to the origin.

Significance

The result itself. Liouville's theorem is the basic structural fact of Hamiltonian dynamics. It rules out asymptotically stable equilibria and attractors of positive measure for Hamiltonian systems. It makes Lebesgue measure invariant, which is the starting point of ergodic theory for mechanical systems. Combined with Theorem 8.11, it gives recurrence for any Hamiltonian motion confined to a bounded energy region. Lemma 8.8 is the quantitative version for arbitrary flows: for the Lorenz equation it gives $V(t) = V e^{-(1+\sigma+b)t}$, so the attractor from Lemma 8.5 has measure zero. Lemmas 8.5 and 8.6 produce attractors and show that they contain the unstable manifolds of their points.

Formalizing it. All of these results are classical and proved in the book. Mathlib has the change-of-variables formula, Poincaré recurrence for conservative measure-preserving maps (MeasureTheory.Conservative), and an $\omega$-limit set for global flows (omegaLimit). It has no flow of a nonlinear ODE with its differentiable dependence on initial conditions, no volume formula along such a flow, and no Hamiltonian formalism. The mission asks for those pieces in the book's local-flow setting, with its hypotheses made explicit.

Difficulty

Lemma 8.8 and Theorem 8.10 need the flow map $x \mapsto \Phi(t, x)$ to be a $C^1$ diffeomorphism of the set of points alive at time $t$ onto its image. They also need its Jacobian to satisfy the first variational equation $\dot\Pi = df(\Phi_t(x))\,\Pi$, whose determinant obeys Liouville's formula for linear systems. None of this is available for a general $C^1$ vector field in Mathlib, which provides local existence and uniqueness of integral curves but not differentiability of the flow in the initial condition. Differentiating $V(t)$ under the integral also needs uniform control on a compact set of initial points. That is why Lemma 8.8 asks the closure of $U$, not just $U$, to be alive at $t_0$. Without that, $\Phi(t_0, U)$ can have infinite volume ($\dot x = x^2$, $U = (0, 1)$, $t_0 = 1$).

Lemmas 8.5 and 8.6 are point-set topology. The obstacle there is the local flow: every statement about $\Phi(t, \cdot)$ must first establish that the points involved are alive at time $t$. The book avoids this by assuming completeness at the start of the chapter. For Lemma 8.7, the Liapunov function $L = rx^2 + \sigma y^2 + \sigma z^2$ from the text has $\dot L \le 0$, not $\dot L < 0$, so convergence to the origin requires the Krasovskii–LaSalle argument, not a plain Liapunov one.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) and phase space is EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with points $(p, q)$, momenta first. volume on it is Lebesgue measure on $\mathbb{R}^{2n}$. The flow is a pair $(I, \Phi)$ satisfying IsMaximalFlow, which makes $t \mapsto \Phi(t, x)$ the unique maximal integral curve on $I_x$. Nothing assumes $I_x = \mathbb{R}$. The chapter's standing completeness assumption is replaced by explicit aliveness hypotheses, and these are implied by completeness. The explicit readings are:

• Theorem 8.10: "Hamiltonian flow" means $H \in C^2$ on an open $\Omega$. "Volume" means Lebesgue measure of any measurable $U \subseteq \Omega$ that is alive at time $t$.
• Lemma 8.8: $f \in C^1$ on $\mathbb{R}^n$. $\overline U$ is alive at $t_0$. The conclusion also states $V(t_0) < \infty$ and integrability of $\operatorname{div} f$ on $\Phi(t_0, U)$, and $V$ is the real-valued volume.
• Theorem 8.11: "region" means a measurable bounded set. "Volume preserving" means that images of measurable subsets of $D$ are measurable and have the same measure. "Any neighborhood $U$" means a neighborhood of some point, hence nonempty. $n \in \mathbb{N}$ means $k \ge 1$.
• Lemma 8.5: a trapping region has $\overline E \subseteq M$ and $\overline E$ forward complete, and "connected" includes nonempty. "Invariant" is two-sided.
• Lemma 8.7: "all solutions converge" includes existence for all $t \ge 0$. The flow is quantified universally.

A trivializing formalization is excluded. The goal is not stated for a complete or globally Lipschitz flow, not for sets of measure zero or bounded open sets only, and not with $\operatorname{div} X_H = 0$ assumed. It must be proved for the flow of $X_H$ built from $H$ itself.

A complete development needs differentiability of the flow in the initial condition and the first variational equation. It also needs Liouville's formula $\det \Pi(t) = \exp \int_0^t \operatorname{tr} A$ for linear systems, and change of variables for the flow map. Each is reusable beyond this mission; contributions of any of them as separate lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012 (cited: author's preliminary version, Chapter 8, pp. 229–241). https://doi.org/10.1090/gsm/140 · https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf
• E. N. Lorenz, Deterministic nonperiodic flow, Journal of the Atmospheric Sciences 20 (1963), 130–141. https://doi.org/10.1175/1520-0469(1963)020%3C0130:DNF%3E2.0.CO;2
• V. I. Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., Graduate Texts in Mathematics 60, Springer, 1989. https://doi.org/10.1007/978-1-4757-2063-1
• The Mathlib Community, Mathlib, Mathlib/Dynamics/Ergodic/Conservative.lean. https://github.com/leanprover-community/mathlib4

Motivation

Fictitious play is the oldest model of learning in games: each player repeatedly best-responds to the empirical frequencies of the opponents' past play. Stochastic fictitious play adds random payoff disturbances before each choice, so that players choose smoothed ("perturbed") best responses. It is a standard model in economics and in the study of learning in games (Fudenberg and Levine, 1998), and its long-run behavior is described through a deterministic mean dynamic, the perturbed best response dynamic, using stochastic approximation theory (Benaïm and Hirsch, 1999).

Supermodular games model strategic complementarities: the gain from moving to a higher strategy increases when opponents move to higher strategies. They arise in coordination, oligopoly and macroeconomic models (Milgrom and Roberts, 1990; Vives, 1990). Hofbauer and Sandholm (Econometrica 2002) show that in such games stochastic fictitious play converges almost surely whenever its mean dynamic has a unique rest point. This mission formalizes that result and the chain of lemmas behind it (Section 5 and the Appendix of the paper).

Timeline. Benaïm and Hirsch (1999) observed that supermodular games with exactly two strategies per player yield strongly monotone perturbed best response dynamics. Hofbauer and Sandholm (2002) extended this to any number of strategies by introducing stochastic dominance coordinates, and proved Theorem 6.1(iv). Benaïm (2000) supplied the low-dimensional convergence theorem used for the dimension ≤ 2 clause.

Setting

A $p$ player normal form game gives player $\alpha$ an ordered finite strategy set $S^\alpha = \{0,\dots,n^\alpha - 1\}$ and a utility $u^\alpha$ on pure profiles. $\Sigma = \prod_\alpha \Delta S^\alpha$ is the set of mixed profiles, and player $\alpha$'s payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\, s^\alpha = i} u^\alpha(s) \prod_{\beta \ne \alpha} x^\beta_{s^\beta}$.

The game is strictly supermodular if for all distinct players $\alpha \ne \beta$ and all profiles $s, \hat s$ with $s^\alpha > \hat s^\alpha$ and $s^{-\alpha} = \hat s^{-\alpha}$, the difference $u^\alpha(s) - u^\alpha(\hat s)$ is strictly increasing in $s^\beta = \hat s^\beta$.

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$, strictly positive, whose choice function $C^\alpha_i(\pi) = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$ is continuously differentiable. The perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$, and the perturbed best response dynamic is

$$(\mathrm P)\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha .$$

$RP(\mathrm P)$ is its set of rest points in $\Sigma$ and $CR(\mathrm P)$ its chain recurrent set.

In standard stochastic fictitious play the shocks $\varepsilon^\alpha_t$ have densities $f^\alpha$ and are independent over time and across players. From an arbitrary initial pure profile $\zeta_1$, each player at time $t+1$ plays the pure strategy maximizing $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where $Z_t = \frac1t \sum_{u \le t} \zeta_u$ is the vector of empirical frequencies.

The stochastic dominance coordinates are $(T^\alpha x^\alpha)_i = \sum_{j > i} x^\alpha_j \in \mathbb R^{n^\alpha - 1}$, the mass on strategies above $i$; $T x \le T y$ means each $y^\alpha$ stochastically dominates $x^\alpha$. In these coordinates (P) becomes a dynamic (T) on $T(\Sigma)$.

Formalization targets

Goal: Theorem 6.1(iv), unique rest point clause

For a strictly supermodular game with $p \ge 2$ players and shock densities as above, if $RP(\mathrm P) = \{x^*\}$ then

$$P\Big(\lim_{t\to\infty} Z_t = x^*\Big) = 1,$$

on every probability space, for every independent shock family with the given densities and every initial profile.

Milestones

• Lemma A.2, eq. (14), Lemma A.3 and eqs. (17)–(18): the order-theoretic and differential facts behind monotonicity.
• Theorem 5.1: $T^{-\alpha} y^{-\alpha} \ge T^{-\alpha} x^{-\alpha} \Rightarrow T^\alpha \tilde B^\alpha(y^{-\alpha}) \ge T^\alpha \tilde B^\alpha(x^{-\alpha})$.
• Theorem 5.2: there are rest points $\underline x, \bar x$ with $RP(\mathrm P) \subseteq [\underline x, \bar x]$.
• Proposition 5.3: (P) and (T) are linearly conjugate.
• Theorem 5.4: (T) is cooperative and irreducible.
• Corollary 5.5(i)–(ii): (P) is strongly monotone, and $CR(\mathrm P) \subseteq [\underline x, \bar x]$, so $CR(\mathrm P) = \{x^*\}$ when the rest point is unique.

Significance

The result gives global almost-sure convergence of a stochastic learning process in a broad class of games with many strategies, where earlier results needed two strategies per player or specific payoff structures. It also shows which properties of the choice function matter: only eqs. (17)–(18), not the symmetry of its derivative used for potential and zero-sum games.

The paper's proof is complete but relies on outside results: stochastic approximation (Benaïm–Hirsch 1999, Benaïm 1999), monotone dynamical systems (Smith 1995), and the inclusion of the chain recurrent set in the global attractor (Robinson 1995). None of these, nor the Hofbauer–Sandholm theorem itself, is formalized in any proof assistant as far as known. The mission produces a machine-checked version of the theorem and of the Section 5 monotonicity theory.

Difficulty

The monotonicity lemmas are finite-dimensional calculus and summation by parts. The substantial steps are elsewhere. Strong monotonicity of a cooperative irreducible system (Corollary 5.5(i)) is a theorem of monotone dynamical systems that Mathlib does not have, and it must hold on the closed, non-open state space $T(\Sigma)$. The step from the ODE to the random process needs the stochastic approximation theorem: the empirical frequencies are an asymptotic pseudotrajectory of (P), and their limit set is almost surely internally chain transitive. Knowing that $x^*$ is globally asymptotically stable for (P) does not by itself give almost-sure convergence of $Z_t$. The limit set of the random process must be related to the chain recurrent set of (P), which is where Corollary 5.5(ii) enters.

Formalization scope

Players are Fin p, strategies Fin (n α) (0-based, same order as the paper), with every $n^\alpha \ge 1$. Mixed profiles live in the ambient space $\prod_\alpha \mathbb R^{n^\alpha}$ with the sup norm. The fields of (P) and (T) are defined on the whole ambient space, so partial derivatives are ordinary Fréchet derivatives. Densities are $[0,\infty]$-valued. Solutions are forward solutions staying in the state space. The chain recurrent set quantifies over solutions, which are unique here because the fields are $C^1$. The process $Z_t$ is defined pathwise from the shocks, with ties in the argmax broken by the smallest index (a null event). Densities may differ across players.

A statement about the ODE (P), or about a single noise law such as logit, would be a different and much weaker theorem. The goal is about the random process $Z_t$, on every probability space carrying independent shocks with the given densities. Irreducibility and strong monotonicity additionally assume that two distinct players each have at least two strategies; when one player owns every stochastic dominance coordinate and has at least two of them, supermodularity holds vacuously while irreducibility fails.

A complete development needs: random utility choice functions and their derivatives; monotone and cooperative ODE theory on convex sets; the chain recurrent set and the global attractor; stochastic approximation for processes with step size $1/t$. The last three are reusable well beyond this mission. Contributions to any milestone, and general-purpose lemmas on cooperative systems or stochastic approximation, are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70 (2002), 2265–2294. https://doi.org/10.1111/1468-0262.00376 (formalized from the authors' manuscript of February 21, 2002)
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Repeated Games, Games and Economic Behavior 29 (1999), 36–72. https://doi.org/10.1006/game.1997.0636
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer (1999). https://doi.org/10.1007/BFb0096509
• M. Benaïm, Convergence with Probability One of Stochastic Approximation Algorithms Whose Average is Cooperative, Nonlinearity 13 (2000), 601–616. https://doi.org/10.1088/0951-7715/13/3/305
• H. L. Smith, Monotone Dynamical Systems, AMS Mathematical Surveys and Monographs 41 (1995). https://doi.org/10.1090/surv/041
• P. Milgrom and J. Roberts, Rationalizability, Learning, and Equilibrium in Games with Strategic Complementarities, Econometrica 58 (1990), 1255–1277. https://doi.org/10.2307/2938316
• D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press (1998).

Motivation

Learning dynamics in games describe how players who repeatedly interact adjust their strategies from observed payoffs. A central question is whether such dynamics lead to Nash equilibrium. For the replicator dynamics, the canonical model of evolutionary game theory, the answer is negative in general: in Matching Pennies and in generic zero-sum games with a unique interior equilibrium, replicator trajectories cycle forever. A classical positive result survives: if a replicator trajectory of a 2-player game stays a bounded distance away from the boundary of the strategy space, its time average converges to the Nash set (Hofbauer and Sigmund, 1998, Ch. 7).

Mertikopoulos and Sandholm (arXiv:1407.6267v2; Math. Oper. Res. 41(4), 2016) study a broad family of continuous-time learning dynamics, regularized reinforcement learning: each player aggregates payoffs into scores and plays the mixed strategy that maximizes score minus a strongly convex penalty function. The family contains the replicator dynamics (entropic penalty) and the projection dynamics (quadratic penalty). For non-steep penalties, trajectories can enter and leave the boundary of the strategy space infinitely often, so the classical "stay away from the boundary" criterion is no longer natural. Section 6 of the paper replaces it with a condition on scores and derives convergence of time averages in zero-sum games with an interior equilibrium.

Setting

A 2-player finite game $\mathcal G$ has players $k = 1, 2$, finite pure strategy sets $\mathcal A_k$, and payoff functions $u_k$ on pure profiles. A mixed strategy $x_k$ is a probability vector on $\mathcal A_k$; $\mathcal X$ is the set of mixed profiles $x = (x_1, x_2)$ and $u_k(x)$ the expected payoff (2.1). The payoff vector of player $k$ is $v_{k\alpha}(x) = u_k(\alpha; x_{-k})$, the payoff of the pure strategy $\alpha$ against the opponent's mixed strategy (2.2). A profile $x^*$ is a Nash equilibrium if no player gains by a unilateral deviation to another mixed strategy; it is interior if $x^*_{k\alpha} > 0$ for every $k$ and $\alpha$. The game is zero-sum if $u_1 = -u_2$.

On the simplex $\Delta$ of a finite set, a penalty function $h$ (Definition 2.1) is continuous on $\Delta$, smooth on the relative interior of every face, and $K$-strongly convex for some $K > 0$:

$$h(tx_1 + (1-t)x_2) \le t h(x_1) + (1-t) h(x_2) - \tfrac12 K t(1-t)\|x_1 - x_2\|^2 .$$

No steepness is required. The choice map is $Q(y) = \arg\max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (Definition 2.2), the convex conjugate is $h^*(y) = \max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (C.1), and the Fenchel coupling is $F_h(p, y) = h(p) + h^*(y) - \langle y|p\rangle$ (C.10).

Each player $k$ has its own penalty function $h_k$. An orbit of (RL) is a pair of trajectories $(y(t), x(t))$, $t \ge 0$, of score vectors and mixed profiles with

$$\dot y_k(t) = v_k(x(t)), \qquad x_k(t) = Q_k(y_k(t)) .$$

The time average of the orbit is $\bar x(t) = t^{-1}\int_0^t x(s)\,ds$.

Formalization targets

Goal: Proposition 6.2 (p. 26)

If $\mathcal G$ is a 2-player zero-sum game with an interior Nash equilibrium, then for every orbit of (RL),

$$\operatorname{dist}\big(\bar x(t), \mathrm{NE}(\mathcal G)\big) \xrightarrow[t\to\infty]{} 0 .$$

The statement fixes no rate and no particular penalty function: it holds for every choice of $h_1, h_2$.

Milestones

1. Proposition C.1 (p. 33): $Q$ is Lipschitz and $Q = dh^*$.
2. Lemma C.6 (p. 36): along (RL), $\frac{d}{dt}F_{h_k}(p_k, y_k(t)) = \langle v_k(x(t)) | x_k(t) - p_k\rangle$.
3. (6.5) (p. 26): in the goal's setting, $F_h(x^*, y(t)) = \sum_k F_{h_k}(x_k^*, y_k(t))$ is constant.
4. Proposition A.1(iii) (p. 31): $Q_\alpha(y) \to 0$ when $y_\alpha - y_\beta \to -\infty$.
5. Proposition C.5 (pp. 35–36): for interior $p$, bounded $F_h(p, y_j)$ forces bounded score differences.
6. Theorem 6.1 (p. 25): in any 2-player game, bounded score differences imply convergence of $\bar x(t)$ to the Nash set.

Significance

The result. Proposition 6.2 shows that the time-average convergence known for the replicator dynamics in zero-sum games is a property of the whole class of regularized reinforcement learning schemes, including those whose trajectories hit the boundary of the strategy space infinitely often, such as the projection dynamics. Time-averaged play of no-regret-type dynamics in zero-sum games is the continuous-time counterpart of the standard argument that averaged learning computes minimax strategies. Theorem 6.1 isolates the mechanism for general 2-player games: bounded score differences suffice, with no zero-sum assumption.

Formalizing it. The results are proved in the paper; none has a machine-checked proof. A complete formalization produces reusable components: differentiability of the conjugate of a strongly convex function on the simplex (a Danskin-type statement), the Fenchel-coupling identity along the dynamics, and a conservation law for zero-sum games. These are the building blocks of many analyses of mirror-descent and follow-the-regularized-leader dynamics.

Difficulty

The first idea, comparing $x(t)$ itself with the equilibrium, fails: $x(t)$ need not converge, and for non-steep penalties it does not stay in the interior, so the Kullback–Leibler argument used for the replicator dynamics is unavailable. The conserved quantity is a function of the scores $y(t)$, not of $x(t)$, and turning its boundedness into control of score differences requires the asymptotic behaviour of the choice map when some scores diverge. The second difficulty is analytic: $h$ is not differentiable at the boundary of $\Delta$, yet $h^*$ must be differentiable everywhere on the score space, with derivative $Q$, for the chain rule along (RL) to apply. Finally, the passage from score differences to the time average uses that $v_k$ is linear in the single opponent's strategy, which is specific to two players.

Formalization scope

• Game. Players are Fin 2, strategy types A k are finite, payoffs are real functions on pure profiles; mixed profiles, expected payoffs and mixed Nash equilibria come from the published agt_games vocabulary (AGT.IsMixedNash). Zero-sum is $u_0(s) + u_1(s) = 0$ for every pure profile; interiority is $x^*_{k\alpha} > 0$.
• Penalty functions. IsPenalty h K is Definition 2.1 with strong convexity in the Euclidean norm; since $K$ is existential the class does not depend on the norm. Steepness is not assumed. Each player has its own $h_k$.
• Choice map and orbits. $x = Q(y)$ is the predicate IsChoice h y x (maximizer of $\langle y|x\rangle - h(x)$ over $\Delta$), never a chosen argmax. An orbit is IsRLOrbit u h y x: for $t \ge 0$, $x_k(t) = Q_k(y_k(t))$ and $\dot y_{k\alpha}(t) = v_{k\alpha}(x(t))$, a right derivative at $t = 0$. This differential form is equivalent to the integral form (RL) because $x$ is continuous along an orbit.
• Time average and convergence. $\bar x(t)$ is defined coordinatewise with the interval integral; only $t \to \infty$ is used. Convergence to the Nash set is Metric.infDist $\to 0$ in the sup metric on profiles. For Theorem 6.1, which has no equilibrium among its hypotheses, the conclusion also asserts that the Nash set is nonempty, because the distance to the empty set is $0$ in Lean.
• Ruled out. A chosen argmax for $Q$, orbits that are vacuous, steepness added to the penalty, convergence of a subsequence or a liminf in place of the limit, and a Nash set that may be empty are all excluded by the encoding. A sorry-free check exhibits a game, penalty functions and an orbit satisfying all hypotheses of the goal, and verifies that Matching Pennies has the interior equilibrium $((\tfrac12,\tfrac12),(\tfrac12,\tfrac12))$.
• Not included. Theorem 6.3 (chain transitivity under the best-response dynamics) depends on the theory of perturbed solutions of differential inclusions, which is not available. Proposition 6.4 is omitted (see the mission notes).

Contributions are welcome on any milestone; Proposition C.1 and Proposition A.1(iii) are self-contained convex-analysis statements about a single penalty function.

Selected references

• P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Mathematics of Operations Research 41(4), 2016. Preprint arXiv:1407.6267v2 (cited version). https://arxiv.org/abs/1407.6267
• J. Hofbauer and K. Sigmund, Evolutionary Games and Population Dynamics, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139173179
• J. Hofbauer, S. Sorin and Y. Viossat, Time average replicator and best-reply dynamics, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0359
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Many engineered and natural systems are networks of identical dynamical units coupled through a directed interaction graph: arrays of oscillators, power grids, sensor and multi-agent networks, gene regulatory circuits. A basic control question for such a network is how to force every unit onto a prescribed reference trajectory (an equilibrium, a periodic orbit or a chaotic solution of a single unit) by acting on only a few of them. Applying a feedback controller to a small fraction of the vertices and letting the coupling spread its effect is called pinning control. It was introduced for scale-free networks by Wang and Chen (2002), shown to work with a single controller on undirected networks by Chen, Liu and Lu (2007), and turned into checkable criteria for undirected networks by Yu, Chen and Lü (2009).

Directed networks are harder. Earlier criteria for directed networks (Zhou, Lu and Lü 2008; Song and Cao 2010) were stated through the symmetric part $G+G^T$ of the coupling matrix, which may have eigenvalues with positive real part even when the network synchronizes, so they lose the structural information of the graph. Yu, Chen, Lü and Kurths (SIAM J. Control Optim., 2013) replaced the standard quadratic Lyapunov function by one weighted with the positive left null vector of the coupling matrix. This mission formalizes their main criterion for strongly connected networks (§3 of the paper) together with the matrix-theoretic lemmas it rests on (§2).

Setting

The network has $N$ vertices with states $x_i(t)\in\mathbb R^n$. A coupling matrix $G=(G_{ij})\in\mathbb R^{N\times N}$ has $G_{ij}\ge 0$ for $i\ne j$ ($G_{ij}>0$ means a connection from vertex $j$ to vertex $i$) and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. The network is strongly connected if any vertex can be reached from any other by a directed path; $G$ is irreducible if no simultaneous permutation of rows and columns brings it to block lower-triangular form $\begin{pmatrix}\tilde G_{11}&0\\\tilde G_{21}&\tilde G_{22}\end{pmatrix}$ with square diagonal blocks of sizes $m$ and $N-m$, $1\le m\le N-1$. The in-degree of vertex $i$ is $k_i^{\mathrm{in}}=\sum_{j\ne i}G_{ij}$.

Each vertex runs the dynamics $\dot x=f(x,t)$ for a continuously differentiable $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$. A reference trajectory $s$ solves $\dot s=f(s,t)$. With coupling strength $c$, inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and control gains $d_i\ge0$ (vertex $i$ is pinned when $d_i>0$), the controlled network is

$$\dot x_i=f(x_i,t)+c\sum_{j=1}^N G_{ij}\Gamma x_j-c\,d_i\Gamma(x_i-s),\qquad i=1,\dots,N.$$

It is globally synchronized if $x_i(t)-s(t)\to0$ for every $i$, every reference trajectory and every solution. The vector field satisfies Assumption 1 if, for a constant matrix $K$,

$$(x-y)^T\bigl(f(x,t)-f(y,t)\bigr)\le(x-y)^TK\Gamma(x-y)\qquad\forall x,y\in\mathbb R^n,\ t\ge0 .$$

For positive weights $\xi_1,\dots,\xi_N$ put $\Xi=\operatorname{diag}(\xi)$, $D=\operatorname{diag}(d)$ and $\widehat G=\tfrac12(\Xi G+G^T\Xi)$.

Formalization targets

Goal: Theorem 3.1 (p. 1402)

Let $f$ satisfy Assumption 1 with $\Gamma$ symmetric, let $G$ be a strongly connected coupling matrix, and let $\xi$ be positive with $\widehat G$ having zero row sums (the weights of Lemma 2.12). If

$$\Xi\otimes\frac{K\Gamma+\Gamma^TK^T}{2}+c\,\widehat G\otimes\frac{\Gamma+\Gamma^T}{2}-c\,(\Xi D)\otimes\frac{\Gamma+\Gamma^T}{2}<0,$$

then the controlled network is globally synchronized.

Milestones

The path to the goal follows the paper: Lemma 2.5 (irreducible $\iff$ strongly connected), Lemma 2.9 ($\rho(A)=\|A\|_\infty$ for nonnegative $A$ with constant row sums), Lemma 2.8 (Perron–Frobenius, already on the platform), Lemma 2.11 (a positive vector $x$ with $G^Tx=0$), Lemma 2.12 (the weights $\Xi$), and the derivative estimate (3.4) for $V=\tfrac12\sum_i\xi_ie_i^Te_i$, $e_i=x_i-s$:

$$\dot V\le e^T\bigl[\Xi\otimes(K\Gamma)+c(\widehat G-\Xi D)\otimes\Gamma\bigr]e .$$

Companion results

Lemma 2.7, Lemma 2.10, and, under the paper's standing assumptions ($K\Gamma=\Gamma K$, $\theta=\lambda_{\max}(\tfrac{K+K^T}{2})\ge0$) with $\Gamma$ positive definite: Corollary 3.2 (the $N\times N$ condition $\theta\Xi+c(\widehat G-\Xi D)<0$ suffices), Corollary 3.3 (i) (an explicit coupling threshold $c>\lambda_{\max}(\theta\Xi)/|\lambda_{\max}(\widehat G-\Xi D)|$), and Corollary 3.4 (the necessary conditions $d_i>\theta/c-k_i^{\mathrm{in}}$ at pinned and $k_i^{\mathrm{in}}>\theta/c$ at unpinned vertices).

Significance

The criterion reduces global synchronization of an $nN$-dimensional nonlinear system to one linear matrix inequality in the data $(G,\Gamma,K,c,D)$, and the corollaries reduce it further to an $N\times N$ inequality and to explicit bounds. Corollary 3.4 turns this into a pinning rule: vertices whose in-degree is below $\theta/c$ must be controlled. Weighting by the left null vector of $G$ is the device that later work on directed consensus and pinning reuses; Lemmas 2.11 and 2.12 isolate it as a statement about Metzler matrices.

The paper's results are proved on paper; none of them has a machine-checked proof that this mission is aware of. A formalization adds three things: a corrected statement of Theorem 3.1 (see the scope section), a Lean library of directed-network matrix facts (irreducibility in the permutation form, its equivalence with strong connectivity, positive left null vectors, the weighted symmetrization $\widehat G$), and a reusable Lyapunov argument for linearly coupled networks with Kronecker-structured quadratic forms.

Difficulty

The obvious first idea, the unweighted Lyapunov function $\tfrac12\sum_ie_i^Te_i$, produces the symmetric part of $G$, which for a directed network need not be negative semidefinite; this is exactly the defect of earlier criteria. The weights must come from a positive left null vector of $G$, whose existence is a Perron–Frobenius statement that needs irreducibility, hence the graph–matrix equivalence of Lemma 2.5. The analytic part needs a derivative of $V$ along solutions on $[0,\infty)$, the conversion of a sum over vertices into a Kronecker quadratic form, and the passage from a negative definite form to convergence of every error component. On the Mathlib side, irreducibility in the paper's permutation sense, spectral radius through characteristic roots, and largest eigenvalues of symmetric matrices all have to be connected to existing API.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n and, for Kronecker products, by pairs (i, a) with $(A\otimes B)_{(i,a),(j,b)}=A_{ij}B_{ab}$; the stacked error uses the same order. Convergence (2.7) is stated with the neighbourhood filter of $0$ in $\mathbb R^n$, which does not depend on the norm. Derivatives are taken within $[0,\infty)$. Pinning is encoded by $d_i>0$ instead of the paper's reordering of the first $l$ vertices. "$M<0$" is positive definiteness of $-M$ (Mathlib PosDef, which includes symmetry); every matrix compared with $0$ is symmetric by construction. $\lambda_{\max}(A)$ of a symmetric matrix is the least $r$ with $v^TAv\le r\,v^Tv$ for all $v$; $\rho(A)$ is the largest modulus of a complex characteristic root. Global synchronization quantifies over every reference solution and every network solution; existence of solutions is not asserted.

Added hypotheses, each disclosed in the item: $\Gamma^T=\Gamma$ in Theorem 3.1 and (3.4), because the printed theorem allows any $\Gamma$ and is then false (a directed 3-cycle with $\Gamma=\begin{pmatrix}1&3\\-3&1\end{pmatrix}$ satisfies (3.2) but its error grows); $c>0$ in Corollary 3.4; at least one pinned vertex in Corollary 3.3 (i); $N\ge1$ in Lemma 2.10. The weights $\Xi$ are not arbitrary: Theorem 3.1 and the corollaries require $\widehat G$ to have zero row sums, which for a coupling matrix is equivalent to $G^T\xi=0$. Assuming the derivative bound (3.4), negative definiteness of $\widehat G-\Xi D$ or decay of $V$ in the goal would trivialize it and is excluded.

The mission needs: graph reachability for matrices with nonnegative off-diagonal entries; Perron–Frobenius for irreducible nonnegative matrices (referenced from the platform); Gershgorin-type bounds; Kronecker products and positive definiteness; and calculus of quadratic forms along solutions. The matrix lemmas (2.5, 2.7, 2.9–2.12) are reusable beyond this mission. Proofs of any item, and alternative proofs of the milestones, are welcome. Corollary 3.3 (ii) is not posed.

Selected references

• W. Yu, G. Chen, J. Lü, J. Kurths, Synchronization via pinning control on general complex networks, SIAM J. Control Optim. 51(2) (2013), 1395–1416. https://doi.org/10.1137/100781699
• X. F. Wang, G. Chen, Pinning control of scale-free dynamical networks, Physica A 310 (2002), 521–531. https://doi.org/10.1016/S0378-4371(02)00772-0
• T. Chen, X. Liu, W. Lu, Pinning complex networks by a single controller, IEEE Trans. Circuits Syst. I 54 (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• J. Zhou, J. Lu, J. Lü, Pinning adaptive synchronization of a general complex dynamical network, Automatica 44 (2008), 996–1003. https://doi.org/10.1016/j.automatica.2007.08.016
• W. Yu, G. Chen, J. Lü, On pinning synchronization of complex dynamical networks, Automatica 45 (2009), 429–435. https://doi.org/10.1016/j.automatica.2008.07.016
• Q. Song, J. Cao, On pinning synchronization of directed and undirected complex dynamical networks, IEEE Trans. Circuits Syst. I 57 (2010), 672–680. https://doi.org/10.1109/TCSI.2009.2024971
• R. Olfati-Saber, R. M. Murray, Consensus problems in networks of agents with switching topology and time-delays, IEEE Trans. Automat. Control 49 (2004), 1520–1533. https://doi.org/10.1109/TAC.2004.834113
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985. https://doi.org/10.1017/CBO9780511810817
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708

Motivation

A self-similar measure on the line is the natural probability measure on the attractor of finitely many contracting similarities $\varphi_i(x)=r_ix+t_i$, chosen with probabilities $p_i$. Self-similar measures are the basic test case for fractal dimension theory; Bernoulli convolutions, the laws of $\sum_j\pm\lambda^j$, are the classical example. When the pieces $\varphi_i(K)$ are well separated, the dimension is given by the entropy-to-Lyapunov formula $H(p)/\chi$. When they overlap, dimension can drop, and the question is exactly how much. If two compositions of the same length coincide as maps (an exact overlap), information is genuinely lost; the entropy-rate dimension conjecture, formulated in Varjú's survey, predicts that this is the only mechanism: the dimension equals $\min\{1,h_{RW}/\chi\}$, where $h_{RW}$ is the entropy rate of the random walk on composed maps.

This mission asks for a formal proof of that formula, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1946–1981 — Moran (Proc. Camb. Phil. Soc. 1946) and Hutchinson (Indiana 1981) give the similarity-dimension formula under separation and the invariant-measure construction.
• 1939–1996 — Erdős proves singularity of Bernoulli convolutions at reciprocal Pisot parameters (AJM 1939); Garsia introduces the entropy rate (Pacific J. Math. 1963); Solomyak proves a.e. absolute continuity (Annals 1995).
• 2009 — Feng and Hu prove exact dimensionality of self-similar measures without separation (CPAM 2009).
• 2014 — Hochman shows a dimension drop forces superexponential concentration of cylinders (Annals 2014).
• 2019 — Breuillard–Varjú (Ann. Probab. 2019) and Varjú's full dimension for transcendental parameters (Annals 2019).
• 2021 — Baker and Bárány–Käenmäki construct systems without exact overlaps whose cylinders approach superexponentially (Adv. Math. 2021, Adv. Math. 2021).
• 2022–2025 — Rapaport proves the no-exact-overlap formula for algebraic ratios (Ann. Sci. ENS 2022); Rapaport–Varjú treat homogeneous three-map systems (Duke 2024); Feng–Feng treat algebraic translations (J. LMS 2025).
• 2026 — Varjú's survey states the entropy-rate conjecture (Conjecture 3, arXiv:2509.22042).
• September 2026 — The OpenAI preprint claims the conjecture in full (Theorem 1.1, p. 2).

Setting

Let $\Lambda$ be a finite nonempty alphabet and $\varphi_i(x)=r_ix+t_i$ with $0<|r_i|<1$, $t_i\in\mathbb R$; different symbols may give the same map, and ratios may be negative and unequal. Let $p=(p_i)$ be a probability vector with all $p_i>0$. The self-similar measure $\mu$ is the Borel probability measure with

$$\mu=\sum_{i\in\Lambda}p_i\,(\varphi_i)_*\mu .$$

For a word $w=i_1\cdots i_n$ let $\varphi_w=\varphi_{i_1}\circ\cdots\circ\varphi_{i_n}$, and let $G_n$ be the random affine map $\varphi_w$ when the letters are independent with law $p$. With logarithms in base $2$,

$$h_{RW}=\inf_{n\ge1}\frac{H(G_n)}{n},\qquad \chi=-\sum_ip_i\log|r_i|>0,$$

where $H$ is Shannon entropy of the distribution of the map $G_n$ (coinciding words are merged). The lower Hausdorff dimension of $\mu$ is $\dim_H\mu=\inf\{\dim_HE: E\ \text{Borel},\ \mu(E)>0\}$. The system has no exact overlaps if distinct words of the same length give distinct maps.

Formalization targets

Milestone: Corollary 6.3 (p. 20) — dimension of the attractor

If there are no exact overlaps, the attractor $K=\{\lim_n\varphi_{\omega_1}\circ\cdots\circ\varphi_{\omega_n}(0)\}$ is compact and nonempty, the equation $\sum_i|r_i|^s=1$ has a unique solution $s_*\ge0$, and $\dim_HK=\min\{1,s_*\}$.

Milestone: Corollary 6.4 (p. 20) — homogeneous systems

If $r_i=\lambda\in(0,1)$ for all $i$ and there are no exact overlaps, then $\dim_H\mu=\min\{1,H(p)/\log(1/\lambda)\}$.

Goal: Theorem 1.1 (p. 2)

For every such family and every strictly positive probability vector $p$,

$$\dim_H\mu=\min\Bigl\{1,\ \frac{h_{RW}}{\chi}\Bigr\}.$$

No separation assumption is made; exact overlaps and repeated generators are allowed.

Significance

The result itself. It removes every arithmetic and separation hypothesis from the dimension theory of self-similar measures on the line: the only way dimension can drop below $\min\{1,H(p)/\chi\}$ is through exact overlaps, and then the drop is exactly measured by the map entropy. Without exact overlaps it gives the classical formula (Corollary 6.2, p. 19), and hence the dimension of every self-similar set without exact overlaps (Corollary 6.3), which is the exact-overlaps conjecture for sets. It asserts nothing about absolute continuity.

Formalizing it. Hausdorff dimension and self-similar measures exist only partially in Mathlib, and the proof needs a quantitative entropy calculus for finite laws at multiple scales. A formal proof would certify the general theorem together with the consequences that previously required separate arithmetic hypotheses. The only external input is the Feng–Hu exact-dimensionality theorem.

Difficulty

Hochman's method yields the formula under exponential separation of cylinders, but Baker and Bárány–Käenmäki showed that without exact overlaps cylinders can still come superexponentially close, so no lower bound on the separation is available, and exact overlaps add further collisions. The proof must therefore detect entropy hidden at arbitrarily fine scales with no control on the smallest positive distance. The preprint does this with a finite-law pair estimate independent of minimal separation (Lemma 3.2, p. 9), conditioning on block types to recover the map-entropy rate when addresses collide (Lemma 4.1, p. 13), and disjoint windows of entropy gain whose depths are chosen adaptively (Section 5).

Formalization scope

• A System ι over a nonempty Fintype ι carries ratio, offset, weight with $0<|r_i|<1$, $p_i>0$, $\sum p_i=1$. SelfSimilar S μ is the equation $\mu=\sum_i p_i\,(\varphi_i)_*\mu$ for a probability measure $\mu$ on $\mathbb R$.
• wordAffine composes maps as $\varphi_{i}\circ\varphi_w$ and records (slope, translation); mapMass merges words with equal complete maps; walkEntropy n is base-2 Shannon entropy of $G_n$; entropyRate is the sInf over $n\ge1$ of $H(G_n)/n$; lyapunov is base-2.
• lowerHausdorffDimension μ is an iInf in ℝ≥0∞ of dimH E over measurable $E$ with $\mu(E)>0$; the goal compares it to ENNReal.ofReal (min 1 (h/χ)).
• NoExactOverlaps is injectivity of wordAffine on all words; words of different lengths always differ in slope modulus, so this matches the same-length condition of the source. The homogeneous milestone allows a single map, a degenerate case where both sides are $0$.
• The attractor milestone uses its own coding map codingPoint and word functions, equivalent to the definitions above.

Selected references

• OpenAI, The entropy-rate dimension formula for self-similar measures on the line, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf
• P. P. Varjú, Entropy rates in the dimension theory of self-similar measures, arXiv:2509.22042 (2026). https://arxiv.org/abs/2509.22042v2
• J. E. Hutchinson, Fractals and self-similarity, Indiana Univ. Math. J. 30 (1981). https://doi.org/10.1512/iumj.1981.30.30055
• D.-J. Feng, H. Hu, Dimension theory of iterated function systems, Comm. Pure Appl. Math. (2009). https://doi.org/10.1002/cpa.20276
• M. Hochman, On self-similar sets with overlaps and inverse theorems for entropy, Ann. of Math. 180 (2014). https://doi.org/10.4007/annals.2014.180.2.7
• P. P. Varjú, On the dimension of Bernoulli convolutions for all transcendental parameters, Ann. of Math. 189 (2019). https://doi.org/10.4007/annals.2019.189.3.9
• E. Breuillard, P. P. Varjú, On the dimension of Bernoulli convolutions, Ann. Probab. (2019). https://doi.org/10.1214/18-AOP1324
• A. Rapaport, Proof of the exact overlaps conjecture for systems with algebraic contractions, Ann. Sci. ENS (2022). https://doi.org/10.24033/asens.2518
• A. Rapaport, P. P. Varjú, Self-similar measures associated to a homogeneous system of three maps, Duke Math. J. (2024). https://doi.org/10.1215/00127094-2023-0019
• S. Baker, Iterated function systems with super-exponentially close cylinders, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107548
• B. Bárány, A. Käenmäki, Super-exponential condensation without exact overlaps, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107549
• B. Solomyak, On the random series Σ±λ^n (an Erdős problem), Ann. of Math. (1995). https://doi.org/10.2307/2118556

Why reentrant lines, and why this one

A reentrant line is a queueing network in which every job follows the same route and visits some stations more than once. It is the standard model of a semiconductor wafer fab, where a wafer returns to the same lithography station for each of its layers (Kumar, Re-entrant lines, Queueing Systems 13, 1993). Because jobs at different stages compete for the same server, a network can be unstable (queues grow without bound) even though every station has nominal load below one; the Lu–Kumar and Rybko–Stolyar examples of the early 1990s made this concrete. Deciding stability under the usual load condition therefore needs an argument specific to the network and to the scheduling policy.

Fluid models turn that question into one about deterministic dynamics. Dai (Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5, 1995) showed that if the fluid model of a queueing discipline is stable, the queueing network under that discipline is positive Harris recurrent. Dai and Weiss (1996) then proved fluid stability, or instability, for several classes of reentrant lines. This mission formalizes their first result, about the smallest reentrant line that revisits a station after visiting another one.

Timeline:

• 1993: Kumar conjectured that the three-buffer line $1 \to 2 \to 1$ is stable under the first-in-first-out (FIFO) discipline whenever the load condition holds, for exponential distributions.
• 1993: Wang proved that the FIFO fluid model of this line is stable, which with Dai's theorem confirms the conjecture.
• 1996: Dai and Weiss (Theorem 3.1) proved stability of the fluid model for every work-conserving discipline, with an explicit emptying time.

Setting

A reentrant line has $I$ stations and $K$ classes. Fluid enters as class $1$ at rate one; class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and service rate $\mu_k = 1/m_k$, and on completion becomes class $k+1$ (class $K$ leaves). 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$.

A fluid model solution is a pair of paths $Q(t) \in \mathbb R^K$ (fluid levels) and $T(t) \in \mathbb R^K$ (cumulative time spent serving 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)\quad(\mu_0T_0(t) = t),\qquad Q_k(t) \ge 0,$$

each $T_k$ starts at $0$ and is nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, with busy time $B_i(t) = \sum_{k \in C_i} T_k(t)$, is nondecreasing. These are the paper's equations (1.8)–(1.12). The solution is work conserving if, in addition, (1.13): $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$.

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

The three-buffer line of Figure 1 has $I = 2$, $K = 3$ and route $1 \to 2 \to 1$: classes $1$ and $3$ at station $1$, class $2$ at station $2$. The load condition (3.1) is

$$\rho_1 = m_1 + m_3 < 1, \qquad \rho_2 = m_2 < 1 .$$

Formalization targets

Goal: Theorem 3.1

$$m_1, m_2, m_3 > 0,\ \ m_1 + m_3 < 1,\ \ m_2 < 1 \ \Longrightarrow\ \text{the work-conserving fluid model (1.8)–(1.13) of } 1 \to 2 \to 1 \text{ is stable.}$$

The goal fixes no emptying time: it asserts only that some $\delta > 0$ works, which is Definition 1.3.

Milestones, in attack order

1. Lemma 2.2 (ii): a nonnegative absolutely continuous $g$ with $\dot g(t) \le -\varepsilon$ almost everywhere where $g(t) > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
2. Display (3.2) (already proved on the platform): at a regular point, the maximum of finitely many functions has the derivative of every component that attains it.
3. Lemma 3.2: for nonnegative linear functions $G_i$ of $Q$ with (a) $\dot G_i \le -\varepsilon_i$ while $W_i > 0$ and (b) $G_i \le \min_{j \ne i} G_j$ while $W_i = 0$, the maximum $G$ is absolutely continuous and nonnegative, and $\dot G(t) \le -\min_i \varepsilon_i$ at regular points with $G(t) > 0$.
4. Drift identity (proof of Theorem 3.1): with $\theta = m_1/(m_1+m_3)$, $G_1 = \theta Q_1^+ + (1-\theta)Q_3^+$ and $G_2 = Q_2^+$, where $Q_k^+ = \sum_{l \le k} Q_l$, one has $G_i(t) = G_i(0) + t - B_i(t)/\rho_i$.
5. Drift rate: $\dot G_i(t) = -(1/\rho_i - 1) < 0$ whenever $W_i(t) > 0$.
6. Condition (b): $W_1(t) = 0 \Rightarrow G_1(t) \le G_2(t)$ and $W_2(t) = 0 \Rightarrow G_2(t) \le G_1(t)$.
7. Emptying time: every work-conserving solution with $|Q(0)| = 1$ is empty from $\max\{\rho_1/(1-\rho_1), \rho_2/(1-\rho_2)\}$ on.

Significance

Theorem 3.1 settles stability of the three-buffer line for every work-conserving discipline at once, not only FIFO. Through Dai's 1995 theorem it gives positive Harris recurrence of the queueing network under any such discipline whose fluid limits satisfy (1.8)–(1.13), under that theorem's distributional assumptions. By the paper's remark after the proof, every other three-buffer reentrant line is feedforward, so with this theorem all three-buffer reentrant lines are stable under every work-conserving policy. The method, a Lyapunov function that is the maximum of linear functions of the fluid levels, recurs in the paper's later theorems (Lu–Kumar network, two-station Kelly-type lines) and in the wider fluid-stability literature.

The result is proved on paper; no machine-checked version exists. The mission's contribution is a formal fluid-model layer for reentrant lines (equations (1.8)–(1.13), Definition 1.3) shared with the other missions of this series, two reusable real-analysis lemmas (Lemma 2.2 (ii) and Lemma 3.2), and a complete formal proof of Theorem 3.1. The fluid-limit theorem linking fluid stability to the stochastic network is cited, not formalized.

Difficulty

The obvious approach is to split cases on the relative loads, as the paper notes ($m_1 + m_3/m_2 < 1$ or not), and track the fluid explicitly; this gives sharp emptying times but requires following solutions through regime changes, which is unwieldy when the discipline is arbitrary. The Lyapunov approach avoids this but moves the difficulty into analysis: the fluid paths are only Lipschitz, so derivatives exist only almost everywhere; the maximum of two Lyapunov components is not differentiable where they cross; and work conservation is a statement about where the idle time can increase, which has to be converted into "the busy time grows at rate one" at points where a station holds fluid. Lemma 2.2 (ii) itself needs the fundamental theorem of calculus for absolutely continuous functions.

Formalization scope

All declarations live in DaiWeissFluid.ThreeBuffer. Committed conventions:

• Classes and stations are 0-based (Fin 3, Fin 2). The paper's class $k$ is Lean k - 1; the line is threeBuffer m with station map ![0, 1, 0], and (3.1) reads m 0 + m 2 < 1, m 1 < 1.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed only for $t \ge 0$, and derivatives are taken at $t > 0$ (HasDerivAt).
• Work conservation (1.13) is in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. This is equivalent to the paper's integral condition for continuous paths.
• No Lipschitz continuity is assumed; it follows from (1.10)–(1.12).
• $m_k > 0$ is an explicit hypothesis (the paper takes it for granted). $|Q(0)| = \sum_k Q_k(0)$.
• Lemma 2.2 (ii) is stated with $\dot g(t) \le -\varepsilon$; the paper prints $<$, but every application uses $\le$, and the stated version is the stronger lemma.
• Lemma 3.2 is stated for any reentrant line with $I \ge 1$ stations, assuming only (1.8)–(1.12), as in the paper.

A trivializing formalization is ruled out: the work-conserving solution set of the three-buffer line is nonempty for every $m$ satisfying (3.1), with $|Q(0)| = 1$ (a sorry-free witness was checked), so the goal is not vacuous, and the goal quantifies over all work-conserving solutions rather than one discipline.

Needed infrastructure: Lipschitz and absolute continuity of the fluid paths, the a.e. fundamental theorem of calculus for absolutely continuous functions (in Mathlib), and the derivative of a finite maximum at a regular point (on the platform as display (3.2)). Lemma 2.2 (ii) and Lemma 3.2 are reusable for the other missions of the series. Proofs of any milestone are welcome independently.

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. 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), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13, 87–110, 1993. https://doi.org/10.1007/BF01158927
• A. N. Rybko and A. L. Stolyar, Ergodicity of stochastic processes describing the operation of open queueing networks, Problems of Information Transmission 28, 199–220, 1992.
• D. D. Botvich and A. A. Zamyatin, Ergodicity of conservative communication networks, Rapport de recherche 1772, INRIA, 1992.