Pensieve header: Searching for a Seifert Formula; continues Seifert.nb at pensieve://People/VanDerVeen/.

Startup

SetDirectory["C:\\drorbn\\AcademicPensieve\\Projects\\SL2Portfolio2"];
(Subscript[PP, _]):=Identity;
<<"Engine-Speedy.m";
<<"Objects.m";
$k=1;
HL[ℰ_] := Style[ℰ, Background -> If[TrueQ@ℰ,Green,Pink]];
ℏ=γ=1;

BS (BanderSnatch)

(See https://en.wikipedia.org/wiki/Bandersnatch)

Define[(Subscript[BS, i,j->k])=(Subscript[C, 1])(Subscript[C, 2])(Subscript[dΔ, i->li,ri])(Subscript[dΔ, j->lj,rj])//(Subscript[(OverBar[dS]), ri])//(Subscript[dS, rj])//(Subscript[dm, li,1->k])//(Subscript[dm, k,rj->k])//(Subscript[dm, k,ri->k])//(Subscript[dm, k,2->k])//(Subscript[dm, k,lj->k])]

Define[(Subscript[tBS, i,j->k])=((Subscript[t2b, i])(Subscript[t2b, j]))//(Subscript[BS, i,j->k])//(Subscript[b2t, k])]

(Subscript[BS, 1,2->3]) // Short

FreeQ[(Subscript[BS, 1,2->3]) , β]

Simplify@(Subscript[tBS, 1,2->3])

Simplify@((Subscript[tBS, 1,2->3])/.(Subscript[𝒜, _])->1)

Simplify@((Subscript[tBS, 1,2->3])/.{(Subscript[𝒜, _])->1,(Subscript[(y|a|x), _])->0})

FreeQ[(Subscript[tBS, 1,2->3]) , τ]

Theorem. tBS is τ-free.
Proof. Follows immediately from the fact that tBS is a “commutator” and (1⊗S)Δ(t)=t⊗1-1⊗t, and that t is central:

Define[(Subscript[tR, i,j])=(Subscript[R, i,j])//(Subscript[b2t, i])//(Subscript[b2t, j]), (Subscript[(OverBar[tR]), i,j])=(Subscript[(OverBar[R]), i,j])//(Subscript[b2t, i])//(Subscript[b2t, j])]

(Subscript[tR, 1,2])

(Subscript[(OverBar[tR]), 1,2])

(Subscript[C, 1])