Read-back: separable_value_decomposition_with_shared_state

What the statement asserts

Fix a natural number $N$ (implicit), a family of types $S_0,\dots,S_{N-1}$ indexed by $i \in \mathrm{Fin}\,N$ (implicit), each assumed finite with decidable equality, and one further type $Z$ (implicit), also assumed finite with decidable equality. The bundle's joint space with a shared coordinate is the product

$$\mathcal{J}_Z \;=\; \Big(\prod_{j \in \mathrm{Fin}\,N} S_j\Big) \times Z ,$$

whose elements are pairs $p = (p_1, p_2)$ with $p_1$ a dependent tuple assigning $p_1(j) \in S_j$ to each index $j$, and $p_2 \in Z$. It is a finite type.

The data are:

• a real square matrix $P$ indexed by $\mathcal{J}_Z$ on both sides, assumed (hP) to be row-stochastic in the bundle's sense (IsTransitionMatrix): all entries $\ge 0$ and $\sum_{q \in \mathcal{J}_Z} P(p,q) = 1$ for every row $p$;
• a real number $\gamma$ with (hγ) $0 \le \gamma$ and (hγ1) $\gamma < 1$ (lower bound non-strict, upper bound strict);
• an arbitrary function $Q : \mathcal{J}_Z \to \mathbb{R}$;
• an arbitrary family of local reward functions $r_i : S_i \times Z \to \mathbb{R}$, one for each index $i$ (no sign or magnitude constraints).

Hypothesis (hQ) says $Q$ satisfies the bundle's Bellman fixed-point condition IsBellmanQ for the transition $P$, the discount $\gamma$, and the reward function $p \mapsto \sum_i r_i(p_1(i), p_2)$; unfolded, this is

$$Q(p) \;=\; \sum_{i \in \mathrm{Fin}\,N} r_i\big(p_1(i),\, p_2\big) \;+\; \gamma \sum_{q \in \mathcal{J}_Z} P(p,q)\, Q(q) \qquad \text{for every } p \in \mathcal{J}_Z .$$

Hypothesis (hsep) uses the bundle's marginal marginalZ: for an index $i$, a source point $p \in \mathcal{J}_Z$ and a target pair $t = (t_1,t_2) \in S_i \times Z$,

$$\mathrm{marg}_i(P)(p, t) \;=\; \sum_{q \in \mathcal{J}_Z} \big[\, q_1(i) = t_1 \ \wedge\ q_2 = t_2 \,\big]\; P(p, q),$$

i.e. the total transition mass from $p$ into the set of joint points whose $i$-th local coordinate is $t_1$ and whose shared coordinate is $t_2$. Hypothesis (hsep) asserts:

for every index $i \in \mathrm{Fin}\,N$ there exists a real matrix $P^{(i)}$ indexed by $S_i \times Z$ on both sides such that, for all $p \in \mathcal{J}_Z$ and all $t \in S_i \times Z$, $\;\mathrm{marg}_i(P)(p,t) = P^{(i)}\big((p_1(i), p_2),\, t\big)$.

That is, each such marginal depends on the source point $p$ only through the pair (agent $i$'s own coordinate, the shared coordinate). Note that $P^{(i)}$ is not assumed to be a transition matrix; nonnegativity and unit row sums follow only on those rows of the form $(p_1(i), p_2)$, and nothing at all is asserted about other rows.

Conclusion. There exists a family of functions $Q_i : S_i \times Z \to \mathbb{R}$, one for each index $i \in \mathrm{Fin}\,N$, such that

$$Q(p) \;=\; \sum_{i \in \mathrm{Fin}\,N} Q_i\big(p_1(i),\, p_2\big) \qquad \text{for every } p \in \mathcal{J}_Z .$$

The existence is plain existence (not unique existence), and the $Q_i$ are required to satisfy nothing beyond this pointwise identity: they are not required to be Bellman fixed points, not tied to the $r_i$ or to the $P^{(i)}$ produced by (hsep), not bounded, and not sign-constrained. Each $Q_i$ is allowed to depend on the shared coordinate $p_2$ as well as on agent $i$'s own coordinate.

Quantification, satisfiability, and degenerate cases

• Every variable occurring in the conclusion is bound. $N$, $S$, $Z$, $P$, $\gamma$, $Q$, $r$ and all typeclass assumptions are binders of the theorem; the only variables inside the conclusion are the existentially bound family $Q_i$ and the universally bound point $p$.
• The hypotheses are jointly satisfiable, so the statement is not vacuous. For example: any $N$, any nonempty finite $S_j$ and $Z$, $P$ the identity matrix on $\mathcal{J}_Z$ (row-stochastic, and its $i$-marginal from $p$ is the indicator of $t = (p_1(i), p_2)$, which depends on $p$ only through that pair, so (hsep) holds), $\gamma = 0$, and $Q(p) = \sum_i r_i(p_1(i), p_2)$, which then satisfies (hQ).
• $\gamma = 0$ is permitted by $0 \le \gamma < 1$; in that case (hQ) reads $Q(p) = \sum_i r_i(p_1(i), p_2)$ outright and (hsep) plays no role in the conclusion. $\gamma$ arbitrarily close to $1$ is permitted; $\gamma = 1$ is not.
• (hQ) presupposes a fixed point of the given Bellman equation exists — $Q$ is supplied as data satisfying it, rather than constructed. Since $P$ is row-stochastic and $0 \le \gamma < 1$ on a finite index type, such a $Q$ exists and is unique whenever $\mathcal{J}_Z$ is nonempty, so (hQ) is a genuine constraint pinning $Q$ down completely rather than an unsatisfiable one.
• $N = 1$ makes the statement trivially satisfiable. With a single index, $\mathcal{J}_Z \cong S_0 \times Z$, the marginal $\mathrm{marg}_0(P)(p,t)$ equals $P(p,t)$ itself and (hsep) holds automatically for every $P$; the conclusion is then satisfied by $Q_0 = Q$ transported along that identification. Likewise if some $S_j$ is a singleton for all $j$ but one.
• $N = 0$: $\mathrm{Fin}\,0$ is empty, so $\prod_j S_j$ is a one-point type and $\mathcal{J}_Z \cong Z$; the reward is the empty sum $0$, (hsep) is vacuous, and the conclusion demands $Q(p) = 0$ (empty sum) for all $p$ — which (hQ) with $\gamma < 1$ and $P$ stochastic does force.
• Empty carriers. If $Z$ is empty, or if any $S_j$ is empty, then $\mathcal{J}_Z$ is empty. In that case (hP), (hQ), (hsep) are all vacuously true (their quantifiers range over an empty type) and the conclusion is vacuously true as well (the required functions exist from the empty type, or the identity is quantified over an empty type). So these instances carry no content but are also not falsified.
• (hsep) is a strong structural restriction on $P$ — it is imposed for every index simultaneously — but it does not force $\mathcal{J}_Z$ or the data to be trivial, as the identity-matrix example above shows.
• The conclusion is an existential over $N$ functions on $S_i \times Z$; when $N \ge 1$ and $Z$ is a singleton it reduces to the requirement that $Q$ be a sum of functions of the individual coordinates.