The prefix differential preserves normality below its cut

Throughout, $M$ is a unital C*-algebra (no order is assumed), $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$. For a cochain $f$ of degree $n+1$, a position $i$ and values $v$ for the other slots, the slice sliceAt f i v is the bounded linear map obtained by letting only slot $i$ vary. A bounded operator $L$ on $M$ has a preadjoint (HasPreadjoint e L) when for each $z\in X$ there is $z'\in X$ with $e^{-1}(L(a))(z)=e^{-1}(a)(z')$ for all $a$, i.e. when it is ultraweakly continuous. For a cochain $h$ of degree $n+1$ and $r\in\mathbb N$, the prefix differential is $d_rh=h^{\mathrm{left}}+\sum_{j\le n,\ j<r}(-1)^{j+1}h^{\mathrm{mid}}_j$ (prefixDifferential h r), where $h^{\mathrm{left}}(v_0,\dots)=v_0h(v_1,\dots)$ and $h^{\mathrm{mid}}_j$ multiplies the inputs $v_j,v_{j+1}$. If every slice of $h$ in a position below $r$ is normal (NormalBefore e h r), then for every position $i\le n$ with $i\le r$, every slice of $d_rh$ (a cochain with $n+2$ slots) at position $i$ has a preadjoint.

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.