A simultaneous right-module average of a finite family of completely bounded maps

Throughout, $M$ is a unital C*-algebra with a partial order making it star-ordered, $X$ is a complex Banach space, and $e:X^*\to M$ is an isometric conjugate-linear isomorphism, so $M$ is a von Neumann algebra with predual $X$ (the Lean hypothesis e). A family $(a_i)$ converges in the predual sense to $b$ (PredualTendsto) when $e^{-1}(a_i)(z)\to e^{-1}(b)(z)$ for every $z\in X$. The hypothesis NoFiniteCentralSummand M says that a central projection $p$ whose corner $pMp$ is finite (every isometry of the corner is unitary) must vanish. Let $M$ be nontrivial with no finite central summand, and let $T_0,\dots,T_n:M\to M$ be bounded linear maps with complete bounds $C_i$. Then there are bounded maps $S_i$ with $\|S_i\|\le C_i$ and $S_i(ab)=S_i(a)b$ for all $a,b$, such that the family $(S_i)$ lies in the weak closure of the simultaneous averages $\bigl(a\mapsto\sum_jT_i(am_j)m_j^*\bigr)_i$ over finite $(m_j)$ with $\sum_jm_jm_j^*=1$ (weakFamilyAverageOrbit).

Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.