A primitive for cocycles multimodular over the algebraic matrix algebra

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$. A cochain of degree $k$ is a bounded complex $k$-linear map $M^k\to M$, and $\partial$ (differentialValue) is the Hochschild differential $(\partial f)(v_0,\dots,v_k)=v_0f(v_1,\dots,v_k)+\sum_{j<k}(-1)^{j+1}f(\dots,v_jv_{j+1},\dots)+(-1)^{k+1}f(v_0,\dots,v_{k-1})v_k$. The hypothesis NoFiniteCentralSummand M says that a central projection $p$ whose corner $pMp$ is finite (every isometry of the corner is unitary) must vanish. A partial isometry (PartialIso) is an element $v$ with $vv^*v=v$; its initial and final projections are $v^*v$ and $vv^*$. Let $M$ be nontrivial with no finite central summand, and let $c_0,c_1,\dots$ be isometries ($c_i^*c_i=1$) with orthogonal final projections whose finite sums tend to $1$ in the predual sense. Let $\mathcal A$ be the *-algebra generated by the elements $c_ic_j^*$ (countableMatrixAlgebra c). Every bounded cocycle $f$ of degree $n+2$ that is $\mathcal A$-multimodular has a bounded primitive: there is $g$ with $\partial g=f$.

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.