Read-back: shared_state_local_transition_deviation

What the statement asserts

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

with elements $p = (p_1,p_2)$, $p_1$ a dependent tuple with $p_1(j) \in S_j$, and $p_2 \in Z$.

The data are: a real matrix $P$ indexed by $\mathcal{J}_Z$ on both sides, assumed (hP) row-stochastic in the bundle's sense (IsTransitionMatrix: all entries $\ge 0$ and every row summing to $1$); an index $i \in \mathrm{Fin}\,N$; a real number $E$ (with no sign hypothesis — $E$ may be negative); and two real matrices $P^{\mathrm{loc}}$ and $P^{\mathrm{true}}$ indexed by $S_i \times Z$ on both sides. Only $P^{\mathrm{loc}}$ is assumed (hPi) to be row-stochastic; $P^{\mathrm{true}}$ carries no such assumption.

The bundle's marginal marginalZ is, for $p \in \mathcal{J}_Z$ and $t = (t_1,t_2) \in S_i \times Z$,

the transition mass from $p$ into all joint points whose $i$-th coordinate is $t_1$ and whose shared coordinate is $t_2$. The two remaining hypotheses are:

• (htrue) for all $p \in \mathcal{J}_Z$ and all $t \in S_i \times Z$: $\;\mathrm{marg}_i(P)(p,t) = P^{\mathrm{true}}\big((p_1(i),p_2),\,t\big)$ — an exact equality, so this marginal depends on $p$ only through the pair $(p_1(i), p_2)$;
• (hE) for all $p \in \mathcal{J}_Z$ and all $t \in S_i \times Z$: $\;\big|\,\mathrm{marg}_i(P)(p,t) - P^{\mathrm{loc}}\big((p_1(i),p_2),\,t\big)\,\big| \le E$ — an entrywise bound (not a total-variation or row-summed bound), with non-strict inequality.

Conclusion. For all $s, t \in S_i \times Z$,

This is again an entrywise, non-strict bound, with the constant $2E$ (twice the constant appearing in (hE), not $E$ itself), and it is quantified over all row indices $s \in S_i \times Z$, not only those arising as $(p_1(i), p_2)$ for some $p \in \mathcal{J}_Z$.

Quantification, satisfiability, and degenerate cases

• Every variable occurring in the conclusion is bound by the theorem's binders ($N$, $S$, $Z$, $P$, $i$, $E$, $P^{\mathrm{loc}}$, $P^{\mathrm{true}}$, plus the typeclass assumptions), and $s,t$ are universally quantified inside the conclusion. However, the constraints on those bound variables are uneven: $P^{\mathrm{true}}$ is pinned down by (htrue) and $E$ by (hE) only on rows of the form $(p_1(i), p_2)$ with $p \in \mathcal{J}_Z$, whereas the conclusion ranges over all rows $s$.
• The hypotheses are jointly satisfiable, so the statement is not vacuous overall. Example: $N = 1$, $S_0$ and $Z$ any nonempty finite types, $P$ the identity matrix on $\mathcal{J}_Z$, $P^{\mathrm{true}}$ and $P^{\mathrm{loc}}$ both the corresponding identity on $S_0 \times Z$, $E = 0$.
• The supplied index $i \in \mathrm{Fin}\,N$ forces $N \ge 1$; the $N = 0$ instance does not exist.
• When $\prod_j S_j$ is nonempty (equivalently, every $S_j$ is nonempty), every pair $(a,z) \in S_i \times Z$ arises as $(p_1(i), p_2)$ for some $p$ — one may take any tuple and overwrite its $i$-th entry with $a$ — so (htrue) and (hE) do constrain every row $s$, and (hE) then forces $E \ge 0$.
• When $\prod_j S_j$ is empty but $S_i \times Z$ is not, the hypotheses constrain nothing while the conclusion still asserts something. Concretely: take $N = 2$, $S_i = \mathrm{Fin}\,1$, $S_j = \varnothing$ for the other index $j$, and $Z = \mathrm{Fin}\,1$. Then $\mathcal{J}_Z$ is empty, so (hP), (htrue) and (hE) hold vacuously for any value of $E$ (including $E = -1$) and any matrix $P^{\mathrm{true}}$, while $S_i \times Z$ is a one-element type on which (hPi) forces $P^{\mathrm{loc}} = (1)$. The conclusion then asserts $|P^{\mathrm{true}}(s,t) - 1| \le 2E$ for the unique $s,t$, with $P^{\mathrm{true}}$ and $E$ unconstrained — e.g. $P^{\mathrm{true}} = (5)$, $E = 0$ gives $4 \le 0$, and $E = -1$ gives a negative right-hand side against a nonnegative left-hand side. So there are instantiations of the binders satisfying all hypotheses in which the conclusion's inequality fails.
• $E$ is a free real parameter with no nonnegativity hypothesis. Whenever $\mathcal{J}_Z$ is empty, (hE) imposes no lower bound on $E$ at all, and $2E$ can be negative.
• $P^{\mathrm{true}}$ is not assumed row-stochastic, nonnegative, or bounded; its only constraint is (htrue), which is vacuous when $\mathcal{J}_Z$ is empty.
• If $S_i \times Z$ is empty (i.e. $S_i$ or $Z$ empty), the conclusion is vacuously true.
• The hypothesis (htrue) is an exact identity, not an approximation, and is imposed for all $p$ and $t$ simultaneously; it is a strong structural restriction on $P$ (its $i$-marginal must factor through $(p_1(i), p_2)$), though it is satisfied e.g. by product-form and identity transitions, so it does not by itself make the statement vacuous.