Separable transitions admit an exact value decomposition

Proved

MarkovEntanglement.separable_implies_value_decomposition

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

markov-decision-processmulti-agent-systemsreinforcement-learningseparabilitytensor-productvalue-decomposition

Statement

Theorem. Consider an $N$ -agent Markov system with joint transition matrix $P^\pi_{1:N}$ on the product state-action space, discount factor $\gamma$ , and rewards that are a sum of local rewards, $r(s,a) = \sum_{i=1}^N r_i(s_i,a_i)$ . Suppose the agents are separable, that is, there are $K \in \mathbb{Z}^+$ , coefficients $\{x_j\}_{j \in [K]}$ with $\sum_j x_j = 1$ , and local transition matrices $\{P^{(j)}_i\}$ such that

P^\pi_{1:N} \;=\; \sum_{j=1}^{K} x_j\, P^{(j)}_1 \otimes P^{(j)}_2 \otimes \cdots \otimes P^{(j)}_N .

Let $Q$ be the solution of the Bellman equation $Q = r + \gamma P^\pi_{1:N} Q$ . Then $Q$ decomposes exactly into local value functions:

Q(s,a) \;=\; \sum_{i=1}^{N} Q_i(s_i, a_i).

Notes

Value decomposition is the standard approximation in multi-agent dynamic programming and reinforcement learning: replace the value of a joint state by a sum of per-agent local values. It underlies index policies for restless multi-armed bandits and a range of modern multi-agent RL architectures, but it is normally used as a heuristic.

This theorem identifies the exact structural condition under which the heuristic is not an approximation at all but an identity: the joint transition matrix must be separable, a finite affine combination of tensor products of local transitions. The name is deliberate — separability here is the direct analogue of separability of a quantum state, and its failure is what the paper calls Markov entanglement.

The converse direction, and the quantitative version that bounds the decomposition error when separability fails, are the other results of this mission. Searchers looking for "when does value decomposition work", "additive value function", "separable transition kernel" or "tensor product of transition matrices" should land here.

Preamble

import Mathlib
import Definitions.Def_markov_entanglement_multi

open scoped BigOperators
open MarkovEntanglement

Formal statement

namespace MarkovEntanglement

theorem separable_implies_value_decomposition
    {N : ℕ} {S : Fin N → Type*} [∀ i, Fintype (S i)] [∀ i, DecidableEq (S i)]
    (P : Matrix (Joint S) (Joint S) ℝ) (hP : IsTransitionMatrix P) (hsep : IsSeparableN P)
    (γ : ℝ) (hγ : 0 ≤ γ) (hγ1 : γ < 1) (r : ∀ i, S i → ℝ) (Q : Joint S → ℝ)
    (hQ : IsBellmanQ P (fun p => ∑ i, r i (p i)) γ Q) :
    ∃ Qi : ∀ i, S i → ℝ, IsValueDecomposition Q Qi := by
  sorry

end MarkovEntanglement

Source

Shuze Chen and Tianyi Peng, *Multi-agent Markov Entanglement*, arXiv:2506.02385v3, Theorem 1, p. 9

Read-back

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

Read-back: `separable_implies_value_decomposition`

What the statement asserts. Fix a natural number $N$ (implicit; $N = 0$ is allowed) and a family of types $S_0, \dots, S_{N-1}$ indexed by $i \in \{0, 1, \dots, N-1\}$ (implicit), each of which is assumed finite and to have decidable equality. Write

\mathcal S \;=\; \prod_{i} S_i

for the joint space: the set of all tuples $p$ assigning to each index $i$ an element $p_i \in S_i$ . The statement then says: for every real matrix $P$ with rows and columns indexed by $\mathcal S$ , every real number $\gamma$ , every family of functions $r = (r_i)_i$ with $r_i : S_i \to \mathbb R$ , and every function $Q : \mathcal S \to \mathbb R$ , if all five of the following hypotheses hold —

$P$ is a row-stochastic matrix: $P_{p,q} \ge 0$ for all $p, q \in \mathcal S$ , and $\sum_{q \in \mathcal S} P_{p,q} = 1$ for every $p \in \mathcal S$ ;
$P$ is separable in the following sense: there exist a natural number $K$ , real coefficients $x_0, \dots, x_{K-1}$ , and matrices $P^{(k)}_i$ (one for each $k < K$ and each index $i$ , with $P^{(k)}_i$ indexed by $S_i \times S_i$ ) such that every $P^{(k)}_i$ is row-stochastic (nonnegative entries, rows summing to $1$ ), the coefficients satisfy $\sum_{k<K} x_k = 1$ , and

P_{p,q} \;=\; \sum_{k<K} x_k \prod_{i} P^{(k)}_i(p_i, q_i) \qquad \text{for all } p, q \in \mathcal S;

note that the $x_k$ are not required to be nonnegative — this is an affine, not necessarily convex, combination, and the equality is exact (no approximation, no limit); since the coefficients must sum to $1$ , $K = 0$ is impossible, so at least one term occurs; 3. $0 \le \gamma$ ; 4. $\gamma < 1$ ; 5. $Q$ satisfies the Bellman fixed-point equation for $P$ , discount $\gamma$ , and the reward function $p \mapsto \sum_i r_i(p_i)$ :

Q(p) \;=\; \sum_{i} r_i(p_i) \;+\; \gamma \sum_{q \in \mathcal S} P_{p,q}\, Q(q) \qquad \text{for all } p \in \mathcal S;

then there exists a family of functions $Q_i : S_i \to \mathbb R$ , one for each index $i$ , such that

Q(p) \;=\; \sum_{i} Q_i(p_i) \qquad \text{for every } p \in \mathcal S.

Binders and what is constrained. $N$ and the family $S$ are implicit universally quantified parameters; the finiteness and decidable-equality assumptions on each $S_i$ are typeclass hypotheses. $P$ , $\gamma$ , $r$ , and $Q$ are explicit universally quantified parameters, together with the five named hypotheses above. The conclusion mentions only $Q$ (bound by the theorem's universal quantifier and pinned by hypothesis 5) and the family $(Q_i)_i$ , which is existentially quantified inside the conclusion. No variable occurring in the conclusion is free or unconstrained. The reward family $r$ does not appear in the conclusion: the asserted $Q_i$ are required only to sum to $Q$ pointwise, and are not required to be related to $r_i$ , to satisfy any local Bellman equation, to be unique, or to be normalized in any way. The matrix $P$ likewise does not appear in the conclusion; hypotheses 1 and 2 bear on the conclusion only indirectly, through the coupling of $Q$ to $P$ in hypothesis 5. The reward is not an arbitrary function on the joint space: it is constructed as $p \mapsto \sum_i r_i(p_i)$ from a given family of per-index functions, so it is additively decomposable by construction, and rewards not of this form are never quantified over.

Joint satisfiability. The hypotheses are simultaneously satisfiable, so the statement is not vacuous. For example, take $N = 1$ with $S_0$ a one-element set, $P$ the $1 \times 1$ matrix $[1]$ (row-stochastic, and separable with $K = 1$ , $x_0 = 1$ ), $\gamma = 0$ , any $r$ , and $Q(p) = r_0(p_0)$ . More generally, for any row-stochastic $P$ and any $0 \le \gamma < 1$ the map $Q \mapsto \big(p \mapsto \sum_i r_i(p_i) + \gamma \sum_q P_{p,q} Q(q)\big)$ is a $\gamma$ -contraction in the supremum norm on the finite-dimensional space $\mathbb R^{\mathcal S}$ , so hypothesis 5 is satisfiable (indeed by exactly one $Q$ ) for every $r$ ; and separable matrices exist (any single tensor product of row-stochastic local matrices, with $K=1$ , $x_0=1$ ).

Degenerate cases the quantifiers include.

$\gamma = 0$ is permitted (hypothesis 3 is non-strict), in which case hypothesis 5 forces $Q(p) = \sum_i r_i(p_i)$ outright.
$N = 0$ : the index set is empty, $\mathcal S$ is the empty product, i.e. a one-element set; every sum $\sum_i(\cdot)$ over indices is $0$ and every product $\prod_i(\cdot)$ is $1$ . Then $P$ is the $1\times1$ matrix $[1]$ , hypothesis 2 holds automatically, hypothesis 5 reads $Q = 0 + \gamma Q$ , and the conclusion reads $Q = 0$ (empty sum) with the empty family of $Q_i$ .
If some $S_i$ is empty (which the assumptions permit, since finiteness does not entail nonemptiness), then $\mathcal S$ is empty, $P$ is the empty matrix, hypotheses 1 and 5 hold vacuously, and the conclusion's universally quantified equation over $p \in \mathcal S$ is vacuous, so the conclusion reduces to the existence of some family $(Q_i)_i$ of functions, which always exists (e.g. the zero functions).
The existential in the conclusion asserts existence only, not uniqueness.

Proof status. The proof body of the declaration is a placeholder; nothing is derived.

Human review

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

View graph

Separable transitions admit an exact value decomposition

Statement

Notes

Read-back: separable_implies_value_decomposition

Read-back: `separable_implies_value_decomposition`