The explicit mean-field map is the mean-field map

Proved

MarkovEntanglement.meanFieldMap_isMeanFieldMap

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

Fix local kernels $P_0, P_1$ on a finite local state space $S$ , a priority index $\nu$ , a system size $N$ and a budget $M$ .

The explicit mean-field map on the simplex,

\varphi(m)_y = \sum_x \big[(m_x - z_x(m))\,P_0(x,y) + z_x(m)\,P_1(x,y)\big], \qquad z_x(m) = \min\Big(m_x, \max\big(0, \alpha - \textstyle\sum_{\nu_y > \nu_x} m_y\big)\Big),

taken at the activation fraction $\alpha = M/N$ , satisfies the characterisation of the mean-field map of the $N$ -agent system: for every joint state $s \in S^N$ and every local state $y$ ,

\varphi(m(s))_y = \frac{1}{N}\sum_{i=1}^N \Big[(1 - p_i)\,P_0(s_i, y) + p_i\,P_1(s_i, y)\Big],

where $m(s)$ is the configuration of $s$ and $p_i$ is the probability with which the index policy activates agent $i$ .

The two descriptions therefore agree on every configuration an $N$ -agent system can actually occupy. This is what licenses proving the asymptotic theorems about the explicit formula, which is defined on the whole simplex, rather than about the characterisation, which pins the map down only on the $1/N$ -lattice.

The proof is a regrouping of the sum over agents into a sum over local states — the agents in a given state are exchangeable, so only their number matters — together with the observation that truncated natural subtraction in the count of activated agents is exactly the $\max(0, \cdot)$ of the continuum formula.

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]

/-- The explicit mean-field map on the simplex agrees, on every configuration an `N`-agent
system can actually occupy, with the characterisation `IsMeanFieldMap` of the previous layer,
provided the activated fraction is `α = M / N`.  This is what licenses proving the asymptotic
theorems about the explicit formula. -/
theorem meanFieldMap_isMeanFieldMap
    (P0 P1 : Matrix S S ℝ) (ν : S → ℝ) (N M : ℕ) (hN : 0 < N) :
    IsMeanFieldMap (N := N) P0 P1 ν M
      (meanFieldMap P0 P1 ν ((M : ℝ) / (N : ℝ))) := by
  sorry

/-! ### M2 — Lemma 7, the mean-field map is piecewise affine -/

end MarkovEntanglement

Source

Shuze Chen and Tianyi Peng, 'Multi-agent Markov Entanglement', arXiv:2506.02385v3, Appendix I, p. 41 (bridging Definition 13 with the mean-field map used in the proof of Theorem 7)

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 matrices $P_0, P_1 : S \times S \to \mathbb{R}$ (arbitrary real matrices — no nonnegativity, no row sums equal to $1$ , no stochasticity of any kind is assumed), every function $\nu : S \to \mathbb{R}$ (arbitrary — ties $\nu(x) = \nu(y)$ are permitted), and every pair of natural numbers $N, M$ subject only to the hypothesis $N > 0$ (in particular $M$ is unconstrained: $M = 0$ is allowed, and $M > N$ is allowed), the following identity holds. Write, for a state assignment $s : \{0,1,\dots,N-1\} \to S$ and $x \in S$ ,

$c_s(x) := \#\{\, i : s_i = x \,\}$ , the number of coordinates in state $x$ , and $m_s(x) := c_s(x)/N \in \mathbb{R}$ (real division, well defined since $N > 0$ );
$h_s(x) := \sum_{y \,:\, \nu(x) < \nu(y)} c_s(y)$ , a natural number, the total count of coordinates sitting in states of strictly higher $\nu$ -value than $x$ ;
$a_s(x) := \min\big(c_s(x),\; M \dot- h_s(x)\big)$ , where $\dot-$ is truncated natural-number subtraction, so $M \dot- h_s(x) = 0$ whenever $h_s(x) \ge M$ ;
$p_s(x) := \dfrac{a_s(x)}{c_s(x)}$ if $c_s(x) \ne 0$ , and $p_s(x) := 0$ if $c_s(x) = 0$ ;

and, for a real-valued function $m : S \to \mathbb{R}$ (not required to be a probability vector) and the specific scalar $\alpha := M/N \in \mathbb{R}$ (real division of the two given naturals; not required to lie in $[0,1]$ ),

$H(m,x) := \sum_{y \,:\, \nu(x) < \nu(y)} m(y)$ ;
$F(m,x) := \min\big(m(x),\; \max(0,\; \alpha - H(m,x))\big)$ ;
$\varphi(m)(y) := \displaystyle\sum_{x \in S} \Big[\big(m(x) - F(m,x)\big)\, P_0(x,y) \;+\; F(m,x)\, P_1(x,y)\Big]$ .

The assertion is that for every $s : \{0,1,\dots,N-1\} \to S$ and every $y \in S$ ,

\varphi\big(m_s\big)(y) \;=\; \sum_{i=0}^{N-1} \frac{1}{N}\Big[\big(1 - p_s(s_i)\big)\, P_0(s_i, y) \;+\; p_s(s_i)\, P_1(s_i, y)\Big].

Note that the left-hand side sums over states $x \in S$ using the continuum quantities $\alpha = M/N$ , $H$ , $F$ applied to the empirical configuration $m_s$ , while the right-hand side sums over the $N$ coordinates $i$ using the integer-arithmetic quantities $h_s$ , $a_s$ , $p_s$ built from counts and truncated subtraction; the claim is that these two expressions agree exactly, as real numbers, for all such $s$ and $y$ . No hypothesis constrains $\nu$ to be injective, constrains $M \le N$ , or asserts any non-degeneracy; the only hypothesis besides the type-class assumptions on $S$ is $N > 0$ . Degenerate cases silently included: $M = 0$ (then $a_s \equiv 0$ , $p_s \equiv 0$ , and $\alpha = 0$ , so $F(m_s, x) = \min(m_s(x), \max(0, -H)) = 0$ when $H \ge 0$ ); $M \ge N$ (then $\alpha \ge 1$ ); states $x$ never visited by $s$ , for which $c_s(x) = 0$ and $p_s(x)$ is defined to be $0$ by the guard rather than by division; and the case where $S$ is empty, in which — since $N > 0$ forces the type of maps $\{0,\dots,N-1\} \to S$ to be empty — the universally quantified statement is vacuously satisfied.

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