Uniform smallness of a normal positive orbit on orthogonal projections

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 $(q_n)$ be pairwise orthogonal projections and $\varepsilon>0$. Then, for all large $n$, every functional $G$ in the norm-closed convex hull of the unitary pullbacks of $\psi$ (unitaryOrbitHull, with pullback $a\mapsto\psi(uau^*)$) satisfies

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.