Local stability at the mean-field fixed point (Lem. 11, Gast et al. 2023)

Proved

MarkovEntanglement.rmab_local_stability

by tianyipeng · Aug 28, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Assume the index policy, through the explicit mean-field map at activation fraction $\alpha$ , satisfies the uniform global attractor property with fixed point $m^\ast$ , and that it is non-degenerate in the mean-field sense: the budget runs out strictly inside some state $x$ , i.e. $0 < \alpha - \sum_{\nu_y > \nu_x} m^\ast_y < m^\ast_x$ . Let $K$ be the matrix of the affine piece of the mean-field map on the priority region of $x$ (Lemma 7). Then:

$K$ is stable on the tangent space of the simplex — its powers contract zero-sum vectors geometrically: there are $C \ge 0$ and $\rho < 1$ with $\|v K^t\|_\infty \le C \rho^t \|v\|_\infty$ for every $v$ with $\sum_x v_x = 0$ . This is the finite-dimensional meaning of "the spectral radius of the linearised dynamics is strictly less than one". The tangent-space formulation is the well-posed one: the hypothesis pins $K$ down only on configurations, which all satisfy $\sum_x m_x = 1$ , so $K$ itself is determined only up to the rank-one gauge $K \mapsto K + \mathbf{1}c^{\top}$ (absorbed by the affine offset $b$ ), and that gauge moves the spectrum arbitrarily — but it acts trivially on zero-sum vectors, which is where the differences $m - m^\ast$ live.
The mean-field iterates reach any prescribed neighbourhood of $m^\ast$ in a number of steps that does not depend on the starting configuration: for every $\varepsilon > 0$ there is a $T$ with $\|\Phi^T(m) - m^\ast\|_\infty < \varepsilon$ for every configuration $m$ in the simplex.

Non-degeneracy is what makes part (1) meaningful. It says that at $m^\ast$ some state is served only fractionally, so $m^\ast$ sits in the interior of its priority region rather than on a boundary between two affine pieces; the map is therefore genuinely affine in a neighbourhood of the fixed point, with linear part acting as $K$ on the differences.

The two parts play complementary roles in the proof of Theorem 7. Part (2) supplies a uniform horizon $\tilde{T}$ after which every trajectory of the mean-field dynamics has entered a small ball around $m^\ast$ ; part (1) then guarantees that once inside, the accumulated amplification of the concentration errors of Lemma 10 no longer grows with the horizon. Together they convert a per-step $1/\sqrt{N}$ fluctuation into an $O(1/\sqrt{N})$ bound on the stationary deviation $\mathbb{E}[\|m - m^\ast\|_\infty]$ .

Preamble

import Mathlib
import Definitions.Def_markov_entanglement_meanfield

open scoped BigOperators
open MarkovEntanglement

Formal statement

namespace MarkovEntanglement

variable {S : Type*} [Fintype S] [DecidableEq S]

/-- Lemma 11 (Local Stability; Lemma C.5 of Gast, Gaujal and Yan 2023).  Under the uniform
global attractor property and mean-field non-degeneracy:

(i) the affine piece of the mean-field map at the fixed point is stable on the tangent space
of the simplex — its powers contract the differences `m − m✦` geometrically, the
finite-dimensional meaning of "spectral radius `< 1`" for the linearised dynamics (the matrix
itself is determined by the dynamics only up to a rank-one gauge that moves the spectrum, so
the tangent-space formulation is the well-posed one);

(ii) the mean-field iterates reach any prescribed neighbourhood of `m✦` in a number of steps
that does not depend on the starting configuration.

Non-degeneracy places `m✦` in the interior of its priority region, so the map is genuinely
affine near the fixed point and (i) is meaningful.  Part (i) is what turns the per-step
concentration of Lemma 10 into a bound that does not blow up with the horizon; part (ii)
supplies the uniform horizon at which to apply it. -/
theorem rmab_local_stability
    (P0 P1 : Matrix S S ℝ) (hP0 : IsTransitionMatrix P0) (hP1 : IsTransitionMatrix P1)
    (ν : S → ℝ) (hν : Function.Injective ν) (α : ℝ) (hα : 0 < α) (hα1 : α < 1)
    (mstar : S → ℝ) (hmstar : IsConfiguration mstar)
    (hUGAP : IsUniformGlobalAttractor (meanFieldMap P0 P1 ν α) mstar)
    (x : S) (hx : 0 < mstar x ∧ 0 < α - higherPriorityMass ν mstar x ∧
      α - higherPriorityMass ν mstar x < mstar x)
    (K : Matrix S S ℝ) (b : S → ℝ)
    (hK : ∀ m : S → ℝ, (∀ z, 0 ≤ m z) → IsPriorityRegion ν α m x →
      meanFieldMap P0 P1 ν α m = fun z => (∑ y, m y * K y z) + b z) :
    IsStableOnTangent K ∧
      ∀ ε > 0, ∃ T : ℕ, ∀ m : S → ℝ, IsConfiguration m →
        supNorm (fun z => meanFieldIterate (meanFieldMap P0 P1 ν α) T m z - mstar z) < ε := by
  sorry

/-! ### M7 — Theorem 7, index policies are asymptotically separable -/

end MarkovEntanglement

Source

Nicolas Gast, Bruno Gaujal and Chen Yan, 'Exponential asymptotic optimality of Whittle index policy' (2023), Lemma C.5; cited as Lemma 11 in Chen and Peng, arXiv:2506.02385v3, Appendix I, p. 43

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Let $S$ be a type with finitely many elements and decidable equality (nothing forces $S$ to be nonempty a priori, but the hypothesis list supplies an element $x : S$ , so $S$ is nonempty in any instance of the statement). Throughout, for a real-valued function $w$ on $S$ write

\|w\|_\infty \;=\; \sup_{z \in S} |w(z)|,

which for a nonempty finite $S$ is the maximum of $|w(z)|$ ; and for $\nu : S \to \mathbb{R}$ , $m : S \to \mathbb{R}$ , $\alpha \in \mathbb{R}$ define the three auxiliary continuum quantities that the statement is built from:

higher-priority mass $\;H(m,z) \;=\; \displaystyle\sum_{\substack{y \in S \\ \nu(z) < \nu(y)}} m(y)$ (sum over exactly those $y$ whose $\nu$ -value is strictly greater than $\nu(z)$ );
activated fraction $\;A(m,z) \;=\; \min\bigl(m(z),\; \max(0,\; \alpha - H(m,z))\bigr)$ ;
mean-field map $\;\Phi(m) : S \to \mathbb{R}$ , $\;\Phi(m)(y) \;=\; \displaystyle\sum_{z \in S}\Bigl[\bigl(m(z) - A(m,z)\bigr)\,{P_0}_{z,y} \;+\; A(m,z)\,{P_1}_{z,y}\Bigr].$

The claim is asserted for every choice of the following data satisfying the following hypotheses:

Two matrices $P_0, P_1 \in \mathbb{R}^{S \times S}$ , each a row-stochastic matrix: all entries $\ge 0$ and every row sums to $1$ .
A function $\nu : S \to \mathbb{R}$ that is injective (distinct states have distinct priority values, so the strict ordering used in $H$ is a total order on the $\nu$ -values).
A real $\alpha$ with $0 < \alpha$ and $\alpha < 1$ .
A function $m^\star : S \to \mathbb{R}$ that is a configuration: $m^\star(z) \ge 0$ for all $z$ , and $\sum_{z \in S} m^\star(z) = 1$ .
$m^\star$ is a uniform global attractor of $\Phi$ , meaning both: (a) $\Phi(m^\star) = m^\star$ as functions on $S$ ; and (b) for every $\varepsilon > 0$ there exists $T_0 \in \mathbb{N}$ such that for every $t \ge T_0$ and every configuration $m$ (i.e. every nonnegative $m$ with $\sum_z m(z) = 1$ ), $\bigl\|\Phi^{t}(m) - m^\star\bigr\|_\infty < \varepsilon$ , where $\Phi^t$ denotes the $t$ -fold iterate of $\Phi$ with $\Phi^0(m) = m$ . The threshold $T_0$ is chosen before $m$ , i.e. uniformly over all configurations.
A distinguished element $x : S$ satisfying all three of: $\;0 < m^\star(x)$ , $\;0 < \alpha - H(m^\star, x)$ , and $\;\alpha - H(m^\star,x) < m^\star(x)$ . (Equivalently $H(m^\star,x) < \alpha < H(m^\star,x) + m^\star(x)$ , so $m^\star$ lies strictly inside the "priority region" of $x$ ; in particular $A(m^\star,x) = \alpha - H(m^\star,x)$ is strictly between $0$ and $m^\star(x)$ .)
A matrix $K \in \mathbb{R}^{S \times S}$ and a function $b : S \to \mathbb{R}$ which together linearize $\Phi$ on the whole priority region of $x$ : for every function $m : S \to \mathbb{R}$ with $m(z) \ge 0$ for all $z$ — note that $m$ is not required to have total mass $1$ here — such that $H(m,x) \le \alpha$ and $\alpha < H(m,x) + m(x)$ (a non-strict inequality on the left, a strict one on the right), one has the exact identity of functions

\Phi(m)(z) \;=\; \Bigl(\sum_{y \in S} m(y)\, K_{y,z}\Bigr) + b(z) \qquad \text{for all } z \in S,

i.e. $\Phi(m) = m K + b$ with $m$ treated as a row vector.

Under all of the above, the statement asserts the conjunction of two claims:

(i) $K$ is stable on the tangent space: there exist real numbers $C$ and $\rho$ with $C \ge 0$ , $\rho \ge 0$ , $\rho < 1$ , such that for every $v : S \to \mathbb{R}$ whose coordinates sum to zero, $\sum_{z \in S} v(z) = 0$ , and for every $t \in \mathbb{N}$ (including $t = 0$ , where $K^0$ is the identity matrix and the bound reads $\|v\|_\infty \le C\|v\|_\infty$ ),

\bigl\| v\,K^{t} \bigr\|_\infty \;\le\; C\,\rho^{t}\,\|v\|_\infty ,

where $v K^t$ is the row-vector–matrix product $(vK^t)(z) = \sum_y v(y)(K^t)_{y,z}$ , and $\rho^0 = 1$ even when $\rho = 0$ .

(ii) For every $\varepsilon > 0$ there exists $T \in \mathbb{N}$ such that for every configuration $m$ (nonnegative with $\sum_z m(z) = 1$ ),

\bigl\|\Phi^{T}(m) - m^\star\bigr\|_\infty \;<\; \varepsilon ,

i.e. the bound is asserted at the single time $T$ only, not for all times $t \ge T$ ; $T$ is again chosen before $m$ , so it is uniform over configurations, and $T = 0$ is not excluded by the statement.

Points worth noting about what the assertion silently includes: neither conclusion mentions $b$ , and conclusion (ii) mentions neither $K$ , $b$ , nor $x$ ; conclusion (ii) is a statement purely about $\Phi$ and $m^\star$ and quantifies only over configurations, so it involves the linearization data not at all. The number $N$ of agents does not occur anywhere; $\alpha$ is a bare real budget fraction, and $\alpha < 1$ is assumed but is not otherwise linked to any of the other data. Hypothesis 7 is a hypothesis about the supplied $K$ and $b$ : if no pair $(K,b)$ satisfies it — for instance if $\Phi$ fails to be exactly affine on the entire set of nonnegative $m$ in the priority region of $x$ , a set that includes $m$ of arbitrarily large total mass — then the statement is vacuously satisfiable for that instance. Conversely, hypothesis 7 is not asserted to determine $K$ uniquely; any $K$ meeting it (and there may be several, differing by a constant row shift absorbed into $b$ ) must satisfy (i). The definition of $\|\cdot\|_\infty$ as a supremum over $S$ returns the junk value $0$ on an empty $S$ , though $x : S$ rules that case out. Finally, hypothesis 5(b) already delivers a statement strictly stronger than conclusion (ii) — for all $t \ge T_0$ rather than at one $T$ — with the same uniformity in $m$ .

Human review

Endorsed by Shuze Chen · Aug 30, 2026
Endorsed by tianyipeng · Aug 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph