The mean-field map is piecewise affine (Lem. 7)

Proved

MarkovEntanglement.meanFieldMap_piecewise_affine

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

Let $\nu$ be an injective priority index on the finite local state space $S$ — the paper's assumption $\nu_1 > \nu_2 > \cdots > \nu_{|S|}$ , which is no loss of generality since state labels may be permuted — and let $\alpha$ be the activation fraction.

Then the mean-field map $\varphi$ of the induced index policy is a continuous function of the configuration, and it is affine on each of the $|S|$ priority regions: for every local state $x$ there are a matrix $K$ and a vector $b$ such that

\varphi(m) = K^{\top} m + b \qquad \text{for every configuration } m \text{ with } \sum_{\nu_y > \nu_x} m_y \le \alpha < \sum_{\nu_y > \nu_x} m_y + m_x.

The region condition says exactly that $x$ is the state in which the budget runs out. Inside it the behaviour of the policy is frozen: every state of strictly higher priority than $x$ is fully activated, every state of strictly lower priority is fully idle, and only $x$ itself is served fractionally, by the amount $\alpha - \sum_{\nu_y > \nu_x} m_y$ — which is linear in $m$ . Injectivity of $\nu$ is what rules out ties, where two states would have to share the residual budget and the map would pick up a genuine minimum.

The affine pieces are what the stability analysis works with: the matrix attached to the region containing the fixed point $m^\ast$ is the linearisation of the dynamics there, and Lemma 11 asserts that it is a stable matrix.

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 7 (Piecewise Affine).  The mean-field map of an index policy is continuous, and on
each of the `|S|` priority regions — the configurations at which a given state is the one the
budget runs out in — it is an affine function of the configuration.  The priority index is
assumed injective, which is the paper's `ν₁ > ν₂ > ⋯ > ν_{|S|}`. -/
theorem meanFieldMap_piecewise_affine
    (P0 P1 : Matrix S S ℝ) (ν : S → ℝ) (hν : Function.Injective ν) (α : ℝ) :
    Continuous (meanFieldMap P0 P1 ν α) ∧
      ∀ x : S, ∃ (K : Matrix S S ℝ) (b : S → ℝ),
        ∀ m : S → ℝ, (∀ z, 0 ≤ m z) → IsPriorityRegion ν α m x →
          meanFieldMap P0 P1 ν α m = fun z => (∑ y, m y * K y z) + b z := by
  sorry

/-! ### M3 — Lemma 8, entanglement is controlled by the configuration's deviation -/

end MarkovEntanglement

Source

Shuze Chen and Tianyi Peng, 'Multi-agent Markov Entanglement', arXiv:2506.02385v3, Appendix I, p. 41, Lemma 7 (adapted from Lemma B.1 of Gast, Gaujal and Yan 2023)

Read-back

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

For every finite type $S$ with decidable equality, every pair of real matrices $P_0, P_1 \in \mathbb{R}^{S\times S}$ , every function $\nu : S \to \mathbb{R}$ that is injective, and every real number $\alpha$ , the following two assertions both hold, where for a vector $m : S \to \mathbb{R}$ and a state $x \in S$ one writes

H_\nu(m,x) \;=\; \sum_{\substack{y \in S \\ \nu(x) < \nu(y)}} m(y), \qquad a_{\nu,\alpha}(m,x) \;=\; \min\bigl(m(x),\ \max(0,\ \alpha - H_\nu(m,x))\bigr),

and where the map $\Phi = \Phi_{P_0,P_1,\nu,\alpha} : (S\to\mathbb{R}) \to (S\to\mathbb{R})$ is defined coordinatewise by

\Phi(m)(y) \;=\; \sum_{x \in S} \Bigl[\bigl(m(x) - a_{\nu,\alpha}(m,x)\bigr)\,(P_0)_{x,y} \;+\; a_{\nu,\alpha}(m,x)\,(P_1)_{x,y}\Bigr]:

(1) $\Phi$ is continuous as a map from $S \to \mathbb{R}$ to $S \to \mathbb{R}$ , both carrying the product topology (for finite $S$ , the usual Euclidean topology on $\mathbb{R}^{|S|}$ ). This is asserted for $\Phi$ on all of $\mathbb{R}^S$ , with no restriction to nonnegative vectors, to probability vectors, or to any region.
(2) For every state $x \in S$ $x \in S$ there exist a matrix $K \in \mathbb{R}^{S\times S}$ $K \in R^{S \times S}$ and a vector $b : S \to \mathbb{R}$ $b : S \to R$ — chosen after $x$ $x$ but before $m$ $m$ , hence uniform in $m$ $m$ — such that for every $m : S \to \mathbb{R}$ $m : S \to R$ satisfying both
- $m(z) \ge 0$ for all $z \in S$ (pointwise nonnegativity only; $\sum_z m(z) = 1$ is not required), and
- the two-sided "priority region" condition at that single state $x$ , namely

H_\nu(m,x) \;\le\; \alpha \quad\text{and}\quad \alpha \;<\; H_\nu(m,x) + m(x)

(weak inequality on the left, strict on the right; imposed at $x$ only, and at no other state),

one has the exact equality of functions

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

i.e. $\Phi(m)$ equals the row-vector–matrix product $mK$ plus the fixed offset $b$ , at every coordinate $z \in S$ .

The statement places no constraints on $P_0$ and $P_1$ beyond being real-valued matrices — they need not be row-stochastic, nonnegative, or related to each other — and none on $\alpha$ beyond being real, so $\alpha$ may be negative or exceed $1$ ; $\nu$ is constrained only by injectivity, which in particular is automatic when $S$ has at most one element. Degenerate readings are included silently by the quantifiers: if $S$ is empty, part (2) is vacuous and $\Phi$ is the unique map on a one-point space, so (1) is trivial; if $\alpha < 0$ , then for nonnegative $m$ one always has $H_\nu(m,x) \ge 0 > \alpha$ , so the hypotheses of (2) are unsatisfiable for every $x$ and any $K, b$ whatsoever discharge the claim; more generally, for any $x$ for which no nonnegative $m$ meets the priority-region condition, part (2) at that $x$ is satisfied vacuously. When the hypotheses are satisfiable they force $m(x) > 0$ , since $H_\nu(m,x) \le \alpha < H_\nu(m,x) + m(x)$ . The conclusion asserts only the existence of such $K$ and $b$ ; it says nothing about their uniqueness, their entries, whether $K$ is stochastic, whether $b$ vanishes, or how $K$ and $b$ vary with $x$ , and it makes no claim about $\Phi$ outside the region described.

Human review

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

View graph