Read-back: value_decomposition_implies_separable

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 assumed finite and equipped with decidable equality. Write

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

for the joint space, whose elements are tuples $p$ with $p_i \in S_i$ for each index $i$. The statement says: for every real matrix $P$ indexed by $\mathcal S \times \mathcal S$ and every real number $\gamma$, if

1. $P$ is row-stochastic: $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$;
2. $0 < \gamma$ (strict);
3. $\gamma < 1$; and
4. the decomposition hypothesis stated in full below holds,

then $P$ is separable, meaning: there exist a natural number $K$, real coefficients $x_0, \dots, x_{K-1}$, and matrices $P^{(k)}_i$ indexed by $S_i \times S_i$ (one for each $k < K$ and each index $i$) such that every $P^{(k)}_i$ is row-stochastic, $\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 .$$

The coefficients $x_k$ are not required to be nonnegative (an affine, not necessarily convex, combination), the equality is exact rather than approximate, and $K = 0$ is impossible because the coefficients must sum to $1$.

The decomposition hypothesis, with its exact quantifier nesting. Hypothesis 4 is, verbatim in structure:

$$\forall\, r = (r_i)_i \ \big(r_i : S_i \to \mathbb R\big),\quad \forall\, Q : \mathcal S \to \mathbb R,\quad \Big[\ \underbrace{\forall p \in \mathcal S,\ Q(p) = \sum_i r_i(p_i) + \gamma \sum_{q \in \mathcal S} P_{p,q} Q(q)}_{\text{antecedent}} \ \Longrightarrow\ \exists\, (Q_i)_i \ \big(Q_i : S_i \to \mathbb R\big),\ \forall p \in \mathcal S,\ Q(p) = \sum_i Q_i(p_i) \ \Big].$$

The nesting is: two universal quantifiers on the outside — first over the family of per-index reward functions $r$, then over the function $Q$ on the joint space — then a single implication whose antecedent is the Bellman fixed-point equation for $P$, discount $\gamma$, and reward $p \mapsto \sum_i r_i(p_i)$, and whose consequent is an innermost existential over a family $(Q_i)_i$ followed by a universal over joint states $p$. Because the existential sits inside both universals, the witnessing family $(Q_i)_i$ is allowed to depend on both $r$ and $Q$; no uniform, linear, or otherwise structured dependence on $r$ is demanded, and no uniqueness of $(Q_i)_i$ is demanded.

What that hypothesis rules in and rules out.

• It ranges only over rewards of the form $p \mapsto \sum_i r_i(p_i)$, built from a family of per-index functions. Joint reward functions on $\mathcal S$ that are not of this additive form are never quantified over, so the hypothesis says nothing about their value functions.
• It ranges over all functions $Q : \mathcal S \to \mathbb R$, but each such $Q$ is filtered by the antecedent. Since $P$ is row-stochastic and $0 < \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}$; hence for each $r$ there is exactly one $Q$ satisfying the antecedent, and the hypothesis is neither vacuous nor over-broad: it asserts precisely that for every additive reward family, the unique discounted Bellman fixed point of $P$ is a pointwise sum of per-index functions of the corresponding coordinate.
• It imposes no relation between the witnessing $(Q_i)_i$ and the given $(r_i)_i$, no local Bellman equation on any $S_i$, and no local transition matrix; it only requires the pointwise additive identity $Q(p) = \sum_i Q_i(p_i)$.
• The same $\gamma$ constrained by hypotheses 2 and 3 appears inside the Bellman equation; the hypothesis makes no claim for any other discount factor.
• Neither $\gamma$, nor $r$, nor $Q$ appears in the conclusion.

Binders and what is constrained. $N$ and the family $S$ are implicit universally quantified parameters, with finiteness and decidable equality as typeclass hypotheses on each $S_i$. $P$ and $\gamma$ are explicit universally quantified parameters, and the four hypotheses above are named premises. In the conclusion, the only variable inherited from the theorem's binders is $P$, which is constrained by hypotheses 1 and 4; the data $K$, $(x_k)_k$, and $(P^{(k)}_i)_{k,i}$ appearing in the conclusion are all existentially quantified inside it. No variable in the conclusion is free or unconstrained.

Joint satisfiability. The hypotheses are simultaneously satisfiable, so the statement is not vacuously true by unsatisfiable premises. For instance, take $N = 1$: then $\mathcal S$ is in bijection with $S_0$ via $p \mapsto p_0$, every function $Q : \mathcal S \to \mathbb R$ is of the form $p \mapsto Q_0(p_0)$, so hypothesis 4 holds for any row-stochastic $P$ and any $\gamma$; choosing any $\gamma \in (0,1)$ satisfies hypotheses 2 and 3. (In that instance the conclusion also holds, with $K = 1$ and $x_0 = 1$.)

Degenerate cases the quantifiers include.

• $N = 0$: the index set is empty, so $\mathcal S$ is the empty product, a one-element set; every sum over indices is $0$ and every product over indices is $1$. Then $P$ is forced by hypothesis 1 to be the $1\times1$ matrix $[1]$, hypothesis 4 asks only that the constant function $Q$ solving $Q = 0 + \gamma Q$ equal the empty sum, and the conclusion holds with $K = 1$, $x_0 = 1$ (the empty tensor product being the all-ones matrix).
• If some $S_i$ is empty — permitted, since finiteness does not imply nonemptiness — then $\mathcal S$ is empty, $P$ is the empty matrix, hypothesis 1 holds vacuously, hypothesis 4 holds vacuously (all equations quantify over $p \in \mathcal S$), and the conclusion also holds trivially: matrix equality over an empty index type is automatic, and a row-stochastic $P^{(k)}_i$ exists for each $i$ (vacuously when $S_i$ is empty, e.g. as a point mass when $S_i$ is nonempty).
• The strictness in $0 < \gamma$ excludes $\gamma = 0$ but the statement is otherwise silent about the boundary $\gamma = 1$, which is excluded by hypothesis 3.

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