Weak compactness of the predual orbit of a normal positive functional

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 $M$ be finite and $\psi$ a positive functional in the predual. Let $\mathcal K$ be the weak-* closure in $M^*$ of the unitary orbit hull of $\psi$ (weakFunctionalClosure (unitaryOrbitHull ...)). Then the preimage of $\mathcal K$ under the canonical map from $X$ with its weak topology to the weak-* dual of $M$ (weakPredualMap e) is compact.

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.