Factorization of a represented completely bounded map

Let $M$ be a nontrivial unital C*-algebra with star-ordered partial order and $H$ a nontrivial complex Hilbert space. Let $\sigma:M\to B(H)$ be a unital *-homomorphism and $T:M\to M$ a bounded linear map with a complete bound $C>0$ (CompletelyBoundedEstimate T C: $\|(T(a_{ij}))\|\le C\|(a_{ij})\|$ for all square matrices). Then $\sigma\circ T$ has an operator factorization with constant $C$ (OperatorFactorization): there are a Hilbert space $K$, a unital *-homomorphism $\pi:M\to B(K)$ and operators $L,R:H\to K$ with $\|L\|\|R\|\le C$ and $\sigma(T(a))=L^*\pi(a)R$ for all $a$.

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.