Read-back — local_transition_deviation_le_two_entanglement

What the statement asserts

Fix a natural number $N$ and a family of types $S_0,\dots,S_{N-1}$ indexed by $\mathrm{Fin}\,N$, each finite and with decidable equality. Write

$$\mathcal J \;=\; \prod_{j\in\mathrm{Fin}\,N} S_j$$

for the joint space (the code's Joint S), whose elements $p$ are functions assigning to each index $j$ a point $p_j\in S_j$; $\mathcal J$ is again a finite type. The claim is: for every

• real matrix $P$ indexed by $\mathcal J\times\mathcal J$ that is row-stochastic — $P_{pq}\ge0$ for all $p,q$ and $\sum_{q\in\mathcal J}P_{pq}=1$ for every $p$ (this is IsTransitionMatrix);
• real-valued $\mu:\mathcal J\to\mathbb R$ that is a strictly positive probability distribution — $\mu(p)>0$ for every $p\in\mathcal J$ and $\sum_{p\in\mathcal J}\mu(p)=1$ (IsPositiveDist);
• with $\mu$ stationary for $P$: $\sum_{p\in\mathcal J}\mu(p)\,P_{pq}=\mu(q)$ for every $q\in\mathcal J$ (IsStationary);
• index $i\in\mathrm{Fin}\,N$ (whose existence forces $N\ge1$);
• two real matrices $\Pi$ and $P^{\mathrm{true}}$ on $S_i\times S_i$ (the code's Pi and Ptrue), both assumed row-stochastic: nonnegative entries and each row summing to $1$;

such that the following two hypotheses hold —

1. (hopt) $\Pi$ attains the infimum defining agent-$i$ entanglement:

$$\sum_{p\in\mathcal J}\mu(p)\cdot\frac12\sum_{t\in S_i}\Bigl|\underbrace{\textstyle\sum_{q\in\mathcal J}[\,q_i=t\,]P_{pq}}_{\texttt{marginalN}}-\Pi_{p_i\,t}\Bigr| \;=\; \varepsilon,$$

where

$$\varepsilon \;:=\; \texttt{entanglementN}\ i\ \mu\ P \;=\; \inf\Bigl\{r\in\mathbb R \;\Bigm|\; \exists\,\Pi'\in\mathbb R^{S_i\times S_i}\ \text{row-stochastic},\ r=\sum_{p\in\mathcal J}\mu(p)\cdot\tfrac12\sum_{t\in S_i}\bigl|\textstyle\sum_{q}[q_i=t]P_{pq}-\Pi'_{p_i t}\bigr|\Bigr\},$$

with $[\,\cdot\,]$ equal to $1$ when the condition holds and $0$ otherwise; 2. (htrue, the definition IsLocalTransitionN) for all $s,t\in S_i$,

$$\Bigl(\sum_{q\in\mathcal J}[\,q_i=s\,]\mu(q)\Bigr)\cdot P^{\mathrm{true}}_{s t} \;=\; \sum_{p\in\mathcal J}\bigl([\,p_i=s\,]\,\mu(p)\bigr)\cdot\Bigl(\sum_{q\in\mathcal J}[\,q_i=t\,]P_{pq}\Bigr),$$

i.e. $P^{\mathrm{true}}$ is the $\mu$-conditional average of the agent-$i$ marginals of $P$ over all joint states whose $i$-th coordinate is $s$, written in cleared-denominator form (both sides multiplied by the $\mu$-marginal at $s$, so no division occurs);

then for all $s,t\in S_i$,

$$\bigl|P^{\mathrm{true}}_{s t}-\Pi_{s t}\bigr| \;\le\; 2\,\varepsilon .$$

This is a bound on a single matrix entry at a time — an absolute difference of two numbers, not a summed or averaged distance — it is asserted uniformly for every pair $(s,t)$, the relation is non-strict $\le$, and the right-hand side is exactly twice the entanglement quantity, independent of $s$ and $t$. Note that the $\mu$-marginal weight $\sum_q[q_i=s]\mu(q)$ that appears on the left of htrue does not appear anywhere in the conclusion.

Everything unfolded

• Joint S $=\prod_j S_j$: functions $p$ with $p_j\in S_j$.
• IsTransitionMatrix A $=$ ($A_{xy}\ge0$ for all $x,y$) and ($\sum_y A_{xy}=1$ for all $x$).
• IsPositiveDist μ $=$ ($\mu(p)>0$ for all $p$) and $\sum_p\mu(p)=1$. Strict positivity everywhere, not mere nonnegativity.
• IsStationary P μ $=$ $\forall q,\ \sum_p \mu(p)P_{pq}=\mu(q)$.
• marginalN i P p t $=\sum_{q}[\,q_i=t\,]P_{pq}$: the probability, from joint state $p$, of landing in any joint state whose $i$-th coordinate is $t$.
• marginalDist i μ s $=\sum_{q}[\,q_i=s\,]\mu(q)$: the push-forward of $\mu$ along the $i$-th coordinate.
• IsLocalTransitionN i P μ Ptrue $=$ the displayed equation (2) above, for all $s,t$.
• muAgentTVDistN i μ P Π $=\sum_{p\in\mathcal J}\mu(p)\cdot\frac12\sum_{t\in S_i}\bigl|\texttt{marginalN}\,i\,P\,p\,t-\Pi_{p_i t}\bigr|$: a $\mu$-weighted average over joint states, not a maximum.
• entanglementN i μ P $=\inf$ of the set of values of muAgentTVDistN over row-stochastic $\Pi'$ — an infimum over a set of reals, which by the order-theoretic convention would return $0$ on an empty or unbounded-below set.
• The bundle's IsSeparableN, tensorProdN, entanglementWith, muTVDist, muNorm, IsProductTransition, rewardEntanglement etc. are not used here: separability of $P$ is never mentioned, and the entanglement quantity used is the agent-$i$, $\mu$-weighted one, not the distance-to-nearest-separable-matrix one.

Which variables are constrained and which are free

• $N$, $S$, $i$: universally quantified; $i:\mathrm{Fin}\,N$ forces $N\ge1$.
• $\mathcal J$ is necessarily nonempty: IsPositiveDist μ demands $\sum_{p\in\mathcal J}\mu(p)=1$, which fails for an empty index type (empty sum $=0$). Hence every $S_j$, in particular $S_i$, is nonempty, and the coordinate map $p\mapsto p_i$ is surjective onto $S_i$. The empty-type degeneracies are therefore excluded by the hypotheses, not left open.
• $P$: constrained to be row-stochastic and to admit $\mu$ as a stationary distribution; otherwise arbitrary (no separability, no product form, no irreducibility, no symmetry).
• $\mu$: constrained to be a strictly positive stationary distribution.
• $P^{\mathrm{true}}$: uniquely determined by $P$, $\mu$ and $i$. Since $\mu>0$ everywhere and $\{q:q_i=s\}\ne\varnothing$ for each $s$, the weight $m(s):=\sum_q[q_i=s]\mu(q)$ is strictly positive, so htrue forces $P^{\mathrm{true}}_{st}=\frac{1}{m(s)}\sum_{p}[p_i=s]\mu(p)\sum_q[q_i=t]P_{pq}$ for every $s,t$. No freedom remains.
• The extra hypothesis hPtrue (that $P^{\mathrm{true}}$ is row-stochastic) is implied by the others: nonnegativity follows from $P\ge0,\mu>0$, and summing htrue over $t$ gives $m(s)\sum_t P^{\mathrm{true}}_{st}=\sum_p[p_i=s]\mu(p)\cdot1=m(s)$, hence unit row sums. It is thus a redundant but consistent assumption, not an additional restriction.
• $\Pi$: constrained to be row-stochastic and to attain the infimum $\varepsilon$. It need not be unique if several minimisers exist; the statement is asserted for whichever minimiser is supplied.
• $s$ and $t$ in the conclusion are universally quantified over $S_i$. No variable in the conclusion is free or unquantified.

Joint satisfiability, degeneracy, and the strength of the hypotheses

• The hypotheses are jointly satisfiable, so the statement is not vacuous. A witness: let every $S_j$ be a nonempty finite type, let $\mu$ be any strictly positive distribution on $\mathcal J$ (e.g. uniform), and let $P_{pq}=\mu(q)$ (rank-one). Then $P$ is row-stochastic and $\mu$ is stationary for it. More generally any irreducible aperiodic row-stochastic $P$ on a finite $\mathcal J$ has a strictly positive stationary $\mu$, so genuinely non-product $P$ satisfying all hypotheses exist; the hypotheses do not force $P$ to be separable or product-form.
• hopt is satisfiable for every such $P,\mu,i$: the set of row-stochastic matrices on $S_i$ is nonempty ($S_i\ne\varnothing$) and compact, and muAgentTVDistN is continuous in $\Pi'$, so its image is compact and the infimum is attained. The infimum is therefore a genuine attained minimum, not the junk value $0$ that the order-theoretic infimum returns on an empty or unbounded-below set. Because $\mu>0$, the infimum satisfies $\varepsilon\ge0$.
• Collapsing cases that the quantifiers include. If $S_i$ is a singleton, both $P^{\mathrm{true}}$ and $\Pi$ are forced to be the $1\times1$ matrix $[1]$ and the conclusion reads $0\le2\varepsilon$ with $\varepsilon=0$. In the rank-one example above, marginalN i P p t does not depend on $p$, the minimiser drives $\varepsilon$ to $0$, and strict positivity of $\mu$ then forces $\Pi=P^{\mathrm{true}}$, so the conclusion again reads $0\le0$. Neither of these is forced in general: the hypotheses admit $\varepsilon>0$.
• Relation between the two sides. Under htrue one has, for each $s,t$, $P^{\mathrm{true}}_{st}-\Pi_{st}=\frac{1}{m(s)}\sum_{p}[p_i=s]\mu(p)\bigl(\texttt{marginalN}\,i\,P\,p\,t-\Pi_{st}\bigr)$, so the left-hand side of the conclusion is naturally controlled by a quantity of the form $\frac{2\varepsilon}{m(s)}$, where $m(s)=\sum_q[q_i=s]\mu(q)\in(0,1]$ is the $\mu$-marginal weight of row $s$. The statement as written omits any such $1/m(s)$ factor: the right-hand side $2\varepsilon$ is uniform over $s$, while $\varepsilon$ is a $\mu$-weighted average over all of $\mathcal J$ (weights summing to $1$) and the left-hand side is an unweighted per-entry deviation at a single row $s$. Whether the hypotheses (row-stochasticity, strict positivity, stationarity, optimality of $\Pi$) suffice to close that gap is exactly the content of the claim and is not something the statement itself assumes.
• No hypothesis is individually vacuous, and none is strong enough to force $\varepsilon=0$ or to force $P^{\mathrm{true}}=\Pi$ in general; the only hypothesis that fully pins down a variable is htrue, which determines $P^{\mathrm{true}}$ from $P$, $\mu$, $i$.