Monotonicity on average under PPT instruments

Let $A,B,C,D$ be finite nonempty types with decidable equality, let $O$ be any type, and let $N_i$, for $i\in O$, be functions from complex matrices on $A\times B$ to complex matrices on $C\times D$. On either bipartite space write $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$. Assume that, for every $i$, both $N_i$ and the function $X\mapsto(N_i(X^\Gamma))^\Gamma$ are represented by complex-linear maps that are completely positive, meaning their identity amplification by every finite reference dimension sends positive semidefinite matrices to positive semidefinite matrices, including reference dimension $0$; also assume $\operatorname{Re}\operatorname{tr}(N_iX)\le\operatorname{Re}\operatorname{tr}X$ for every $X\ge0$. Assume further that there is a function $T$ represented by finitely many Kraus matrices $K_j$, so that $T(X)=\sum_jK_jXK_j^\dagger$ and $\sum_jK_j^\dagger K_j=I$, such that $\sum_{i\in O}N_iX=T(X)$ for every matrix $X$, with convergence understood as the net of sums over finite subsets of $O$. Let $\rho\ge0$ have trace $1$, and, for any bipartite matrix $X$, define

using the Euclidean operator norm and matrices $R$ on the same space as $X$. Set $p_i=\operatorname{Re}\operatorname{tr}(N_i\rho)$, and define $c_i=p_iW(p_i^{-1}N_i\rho)$ if $p_i>0$, and $c_i=0$ otherwise. The theorem asserts $0\le W(\rho)$ and the existence of a real $s$ such that $\sum_{i\in O}c_i=s$, again as a net of finite-subset sums, and $s\le W(\rho)$. No finiteness or countability assumption is imposed on $O$.