Pensieve header: Testing if KV is equivalent to R4 + Unitarity of $\Phi_V$.

SetDirectory["C:\\drorbn\\AcademicPensieve\\Projects\\WKO4"];
<< FreeLie.m;
<< AwCalculus.m;
Rs[a_,b_]:= Es[⟨a->LS[0], b->LS[LW@a]⟩, CWS[0]];
α=LS[{x,y}, αs]; β=LS[{x,y}, βs];γ=CWS[{x,y}, γs];
V=Es[⟨x->α, y->β⟩, γ];
R4Eqn=V**(Rs[x,z] // dΔ[x,x,y]) ≡ Rs[y,z]**Rs[x,z]**V ;
(Subscript[V, 12])=V//dσ[{x,y}->{1,2}];
(Subscript[Φ, V]) = ((((Subscript[V, 12])//dA))^(σ[12,3]))**((((Subscript[V, 12])//dA))^(σ[1,2]))**((Subscript[V, 12])^(σ[2,3]))**((Subscript[V, 12])^(σ[1,23]));
UnitarityOfPhi = ((Subscript[Φ, V])**dA[(Subscript[Φ, V])])≡Es[⟨1->LS[0], 2->LS[0],3->LS[0]⟩,CWS[0]];
βs[x]= 1/2; βs[y]=0;
SeriesSolve[{α, β,γ}, ((ℏ^(-1))R4Eqn) &&UnitarityOfPhi ];
V

V@{7} // Timing

(Subscript[Φ, V])