Pensieve header: Verifying the “Big G Lemmas”.

Implementing (Subscript[g, 1])

ϵ /: (ϵ^2)=0;
PBWRule={u->1,c->2,w->3};
B[U@c,U@w]=-(B[U@w,U@c]=U@w);
B[U@u,U@c]=-(B[U@c,U@u]=U@u);
B[U@w,U@u]=-(B[U@u,U@w]=b U[]-2ϵ U@c);

UU[l___,((x_)^(n_)),r___]:= UU[l,Sequence@@Table[x,{n}],r];
UU[l___,1,r___]:= UU[l,r];
UU[]=U[]; UU[l_,r___]:=U[l]**UU[r];(Subscript[U, i_])[ℰ_] := ℰ /. {b->(Subscript[b, i]), u_U :> Replace[u, x_ :> (Subscript[x, i]),1]};

B[x_,x_]=0;
B[U[(Subscript[(x_), i_])],U[(Subscript[(y_), i_])]]:=B[U[(Subscript[x, i])],U[(Subscript[y, i])]]=(Subscript[U, i])[B[U@x,U@y]];
B[U[(Subscript[(x_), i_])],U[(Subscript[(y_), j_])]] /; i=!=j := 0;
B[x_,y_] := x**y-y**x;

x_⪯y_:=OrderedQ[{x,y}/.PBWRule]; x_≺y_:=!OrderedQ[{y,x}/.PBWRule];
Simp[ℰ_]:= Collect[ℰ, _U, Expand];

Unprotect[NonCommutativeMultiply];
NonCommutativeMultiply[x_] := x;
0**_=_**0=0;
x_**U[]:=x; U[]**x_:=x;
(a_*x_U)**(b_*y_U) := If[a b === 0, 0, Simp[a b (x**y)]];
(a_*x_U)**y_ := Simp[a(x**y)]; x_**(a_*y_U) := Simp[a(x**y)];
(x_Plus)**y_ := (#**y)& /@ x; x_**(y_Plus) := (x**#)& /@ y;
U[x_]**U[y_] := If[x≺y, U[x,y], U[y,x]+B[U@x,U@y]];
U[x_] ** U[y1_,yy__] := If[x⪯y1,U[x,y1,yy],(U@x**U@y1)**U@yy];
U[xx__,xn_]**U[yy__] := U@xx**(U@xn**U@yy);

U[l___,((x_)^(n_)),r___]:= U[l,Sequence@@Table[x,{n}],r];
U[l___,1,r___]:= U[l,r];

𝕆[n_, poly_, specs___] := Module[{vs,us},
vs=Join@@(First /@ {specs});
us=Join@@({specs} /. (l_->s_) :> (l/.(Subscript[x_, i_]):>(Subscript[x, s])));
Total[
CoefficientRules[Normal@Series[poly, {ℏ,0,n}], vs] /. (p_->c_) :> c UU@@((us^p))
]
]

Testing (Subscript[g, 1])

LBasis[n_Integer] := LBasis[Range[n]];
LBasis[S_] := DeleteCases[0]@Module[{i,j,k,l}, SortBy[(# /. {ϵ->2,(Subscript[c, _])->2,(Subscript[u, _])->2,(Subscript[w, _])->2, U->Times})&][
Union@Flatten[{{U[],ϵ U[]},
Table[{U@(Subscript[c, i]),U@(Subscript[u, i]),U@(Subscript[w, i]),ϵ U@(Subscript[c, i]),ϵ U@(Subscript[u, i]),ϵ U@(Subscript[w, i])}, {i,S}],
Table[{U[(Subscript[u, i]),(Subscript[w, j])],ϵ U[(Subscript[u, i]),(Subscript[w, j])],ϵ U@@Sort@{(Subscript[c, i]),(Subscript[c, j])},ϵ U[(Subscript[u, j]),(Subscript[c, i])],ϵ U[(Subscript[c, i]),(Subscript[w, j])]}, {i,S}, {j,S}],
Table[{ϵ U[(Subscript[u, j]),(Subscript[c, i]),(Subscript[w, k])],ϵ U@@Sort@{(Subscript[u, i]),(Subscript[u, j]),(Subscript[w, k])},ϵ U@@Sort@{(Subscript[u, i]),(Subscript[w, j]),(Subscript[w, k])}}, {i,S}, {j,S},{k,S}],
Table[ϵ U@@Sort@{(Subscript[u, i]),(Subscript[u, j]),(Subscript[w, k]),(Subscript[w, l])}, {i,S}, {j,S},{k,S},{l,S}] }]
]]

bas=LBasis[2];
Table[B[x,y]+B[y,x], {x,bas},{y,bas}] //Flatten//Union

bas=LBasis[2]; Timing[
Table[
{x,y,z}=xyz;
Simp[B[B[x,y],z]+B[B[y,z],x]+B[B[z,x],y]],
{xyz, Subsets[bas,{3}]}
] //Flatten//Union
]

Testing the Big (Subscript[𝔤, 0])/(Subscript[𝔤, 1]) Lemmas

c Relations  (of (Subscript[𝔤, 0])/(Subscript[𝔤, 1])).

With[{n=10}, Simp[
𝕆[n, (E^(ℏ(γ (Subscript[c, 0])+β (Subscript[u, 0])))),{(Subscript[c, 0]),(Subscript[u, 0])}->0]==𝕆[n, (E^(ℏ(γ (Subscript[c, 0])+(E^(ℏ γ))β (Subscript[u, 0])))),{(Subscript[u, 0]),(Subscript[c, 0])}->0]
]]

With[{n=10}, Simp[
𝕆[n, (E^(ℏ(γ (Subscript[c, 0])+ℏ β (Subscript[w, 0])))),{(Subscript[w, 0]),(Subscript[c, 0])}->0]==𝕆[n, (E^(ℏ(γ (Subscript[c, 0])+ℏ (E^(ℏ γ))β (Subscript[w, 0])))),{(Subscript[c, 0]),(Subscript[w, 0])}->0]
]]

The Weyl Relations (of (Subscript[𝔤, 0]))

With[{n=10}, Simp[
𝕆[n, (E^(ℏ(α (Subscript[w, 0])+β (Subscript[u, 0])))),{(Subscript[w, 0]),(Subscript[u, 0])}->0]==𝕆[n, (E^(ℏ(-ℏ α β (Subscript[b, 0])+α (Subscript[w, 0])+β (Subscript[u, 0])))),{(Subscript[u, 0]),(Subscript[w, 0])}->0] /. ϵ->0
]]

The Emergence of ν (in (Subscript[𝔤, 0]))

With[{n=10, ν=(((1+ℏ (Subscript[b, 0])δ))^(-1))}, Simp[
𝕆[n,(E^(ℏ δ (Subscript[u, 0])(Subscript[w, 0])))(E^(ℏ β (Subscript[u, 1]))),{(Subscript[w, 0]),(Subscript[u, 0]),(Subscript[u, 1])}->0]==𝕆[n,(E^(ℏ δ (Subscript[u, 0])(Subscript[w, 0])))(E^(ℏ ν β (Subscript[u, 1]))),{(Subscript[u, 1]),(Subscript[w, 0]),(Subscript[u, 0])}->0] /. ϵ->0
]]

Reversing a quadratic (in (Subscript[𝔤, 0]))

With[{n=10, ν=(((1+ℏ (Subscript[b, 0])δ))^(-1))}, Simp[
𝕆[n,(E^(ℏ δ (Subscript[u, 0])(Subscript[w, 0]))),{(Subscript[w, 0]),(Subscript[u, 0])}->0]==𝕆[n,ν (E^(ℏ ν δ (Subscript[u, 0])(Subscript[w, 0]))),{(Subscript[u, 0]),(Subscript[w, 0])}->0] /. ϵ->0
]]

The main (Λóγοϛ) relation (of (Subscript[𝔤, 1]))

Λ=(1/2) (ν (Subscript[b, 0]) (-2 (δ^2)-4 α β δ ν-(α^2) (β^2) (ν^2)+(α^2) (δ^2) (ν^2) (Subscript[w, 0]^2)+4 (δ^2) ν (Subscript[u, 0]) (Subscript[w, 0]) (δ+α β ν+α δ ν (Subscript[w, 0]))+(δ^2) (ν^2) (Subscript[u, 0]^2) ((β^2)+4 β δ (Subscript[w, 0])+3 (δ^2) (Subscript[w, 0]^2)))+2 (2 (Subscript[c, 0]) (δ+α β ν+α δ ν (Subscript[w, 0])+δ ν (Subscript[u, 0]) (β+δ (Subscript[w, 0])))+(ν^2) (2 δ+α β ν+α δ ν (Subscript[w, 0])+δ ν (Subscript[u, 0]) (β+δ (Subscript[w, 0]))) (α (Subscript[w, 0])+(Subscript[u, 0]) (β+2 δ (Subscript[w, 0])))));
With[{n=10}, Simp[
𝕆[n,(E^(α (Subscript[w, 0])+β (Subscript[u, 0])+δ (Subscript[u, 0])(Subscript[w, 0])))/.{α->ℏ α, β->ℏ β,δ->ℏ δ},{(Subscript[w, 0]),(Subscript[u, 0])}->0]==
𝕆[n,ν(1+ϵ ν Λ)(E^(ν(-(Subscript[b, 0])α β+α (Subscript[w, 0])+β (Subscript[u, 0])+δ (Subscript[u, 0])(Subscript[w, 0]))))/.{ν->(((1+(Subscript[b, 0])ℏ δ))^(-1)), α->ℏ α, β->ℏ β,δ->ℏ δ},{(Subscript[u, 0]),(Subscript[c, 0]),(Subscript[w, 0])}->0]
]]

Λ1=Total[CoefficientRules[Λ/.{(Subscript[x_, 0]):>x}, {u,c,w}] /. (p_->cc_) :> Simplify[cc]Times@@(({u,c,w})^p)]

Λ1//TeXForm