A faithful normal tracial state from a state faithful on central 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 (FiniteAlgebra M) and $\psi$ a positive functional in the predual (TraceInPredual e ψ) with $\psi(1)=1$ that does not vanish on nonzero central projections. Then there is a positive functional $\tau$ in the predual with $\tau(1)=1$, $\tau(ab)=\tau(ba)$, and $\tau(a^*a)=0\Rightarrow a=0$.

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.