A primitive for last-slot normal cocycles under finite path tests

Throughout, $M$ is a unital C*-algebra with a partial order making it star-ordered, $X$ is a complex normed space (completeness is not assumed), and $e:X^*\to M$ is an isometric conjugate-linear isomorphism (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$. Let $X$ be separable, and let $\tau$ be a faithful tracial positive functional in the predual with $\tau(1)=1$, with left and right multiplications having preadjoints. Assume the finite path tests (FinitePathTests τ): for finite data consisting of fixed unitaries indexed by $C$, words in unitaries indexed by $C\sqcup D$ in which each row $i$ contains a letter $a_i\in D$ that occurs at exactly one position of the whole array, and nontrivial reduced words $q$, for each $\varepsilon>0$ one can choose unitaries for $D$ making all traces $|\tau(q(\text{paths}))|<\varepsilon$. Let $f$ be a bounded cocycle of degree $n+1$ whose last slot is normal: $x\mapsto f(a,x)$ has a preadjoint for each $a$. Then there is $g$ 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.