Homogeneous type I algebras with an abelian diagonal unit have bounded primitives

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). Let $E=(e_{ij})_{i,j<d}$ be a matrix system with $e_{ij}^*=e_{ji}$, $e_{ij}e_{kl}=\delta_{jk}e_{il}$ and $\sum_ie_{ii}=1$ (MatrixSystem M d), and suppose some diagonal unit $e_{ii}$ is an abelian projection (FinitePathMain.AbelianProjection). Then every bounded cocycle $f$ of degree $n+1$ on $M$ has a primitive $g$ of degree $n$ with $\|g\|\le\|f\|$ and $\partial g=f$. Here 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$.

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.