A row of partial isometries reaching the central support of a projection

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)(x)\to e^{-1}(b)(x)$ for every $x\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$. A partial isometry (PartialIso) is an element $v$ with $vv^*v=v$; its initial and final projections are $v^*v$ and $vv^*$. Let $p$ be a projection with central support $z$ (IsCentralSupport p z: $z$ is a central projection, $p\le z$, and any central projection $c$ with $cp=0$ has $cz=0$). Then there is a set $S$ of partial isometries with $vv^*\le p$ and $v^*v\le z$ for $v\in S$, with pairwise orthogonal initial projections, such that

in the predual sense.

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.