No abelian corners implies the finite path tests

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$. Here $\tau$ is a positive linear functional on $M$ with $\tau(1)=1$ that lies in the predual (TraceInPredual: $\tau(x)=\overline{e^{-1}(x)(z)}$ for some $z\in X$), is tracial, and is faithful ($\tau(a^*a)=0$ implies $a=0$), and $\|x\|_2=\tau(x^*x)^{1/2}$ is the norm of τ.toPreGNS x. The hypothesis NoAbelianCorners M says that for every nonzero projection $p$ the corner algebra $\{a:pa=a=ap\}$ contains two noncommuting elements. If NoAbelianCorners M holds, then $\tau$ satisfies the finite path tests (FinitePathTests τ): given finite types $C,D\neq\emptyset,T$, unitaries $(v_c)_{c\in C}$, for each $t\in T$ a word pattern $w_t$ in $(C\sqcup D)\times\{\pm\}$ in which each row $i$ contains a letter $a_i\in D$ that occurs at exactly one position of the whole array $w_t$, a nontrivial reduced word $q_t$ in the rows, and $\varepsilon>0$, there are unitaries $(u_d)_{d\in D}$ with

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.