Countably many orthogonal isometries summing to one in the properly infinite case

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$. 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^*$. If $M$ has no finite central summand, there is a sequence $c_0,c_1,\dots$ of partial isometries with $c_i^*c_i=1$, with $(c_ic_i^*)(c_jc_j^*)=0$ for $i\ne j$, and with

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.