Pensieve header: A unified verification testing suite for the $sl_2$-portfolio project, Uxi version. Continues pensieve://Projects/SL2Portfolio/nb/Verification.pdf.

Also continues pensieve://Projects/PPSA/nb/Verification.pdf and pensieve://2017-06/ and pensieve://2017-08/.

Prolog

wdir=SetDirectory["C:\\drorbn\\AcademicPensieve\\Projects\\SL2Portfolio"];
<< "SL2PortfolioProgram.m"

$p=2; $k=1; $U=QU;

HL[ℰ_] := Style[ℰ, Background -> Yellow];

DocileQ

DQ/@{(ϵ^2)x y (Subscript[a, 2]), (ϵ^2)(x^2)(y^3)}

Initialization / Utilities

HL[(Subscript[DP, x->(Subscript[D, ξ]),y->(Subscript[D, η])])[(x^2)(y^3)][(E^(δ ξ η))]==6 (E^(δ η ξ)) (δ^3) ξ+6 (E^(δ η ξ)) (δ^4) η (ξ^2)+(E^(δ η ξ)) (δ^5) (η^2) (ξ^3)]

(Subscript[SP, {ξ->x}])[((ξ^2)+ξ+3)((x^5)(E^x)+7x)+99a]

(Subscript[SP, {ξ->x,η->y}])[((ξ^2)+ξ+3+2ξ η)((x^5)(E^x)+7x)+99a+(E^(δ x y))ξ η]

Implementing CU=𝒰((Subscript[sl, 2]^(γϵ)))

Verify σ and Δ! Also Generalize Δ to (Subscript[Δ, i,(Subscript[j, 1]),(Subscript[j, 2]),...]).

Verifying associativity on triples of generators:

With[{bas=CU/@{y,a,x}},
Table[z1**(z2**z3)-(z1**z2)**z3 // Simp // HL,
{z1,bas},{z2,bas},{z3,bas} ] ]

Verifying associativity on a “random” triple:

With[{z1=CU[y,y,a,a,x,x], z2=CU[y,a,x], z3=CU[y,y,a,x]}, {
(rhs=(z1**z2)**z3 // Simp) // Short,
z1**(z2**z3)-rhs // Simp //HL
}]// Timing

Implementing QU=(Subscript[𝒰, q])((Subscript[sl, 2]^(γϵ)))

Series[(1-T (E^(-2ϵ a ℏ)))/ℏ, {a,0,3}]

HL/@DQ/@Series[{(1-T (E^(-2ϵ a ℏ)))/ℏ, (E^(ℏ ϵ a))}, {ϵ,0,5}]

With[{bas=QU/@{y,a,x}},Table[{z1,z2}->Simp[z1**z2-z2**z1],{z1,bas},{z2,bas}] ]

Verifying associativity on triples of generators:

With[{bas=QU/@{y,a,x}},
Table[HL[z1**(z2**z3)-(z1**z2)**z3] // Simp,
{z1,bas},{z2,bas},{z3,bas} ] ]

Verifying associativity on a “random” triple (~34 secs @ $p=5, $k=2):

With[{z1=QU[y,y,a,a,x,x], z2=QU[y,a,x], z3=QU[y,y,a,x]}, {
(rhs=(z1**z2)**z3 // Simp) // Short,
HL[z1**(z2**z3)-rhs // Simp ]
}]// Timing

Verifying that (Subscript[Lim, ℏ->0])QU=CU using a “random” product (~23 secs @ $p=5, $k=2):

With[{z1=CU[y,y,a,a,x,x], z2=CU[y,a,x], z3=CU[y,y,a,x]}, {
Short[lhs=z1**(z2**z3)],
Short[rhs=(QU@@z1)**((QU@@z2)**(QU@@z3))],
Expand[Limit[rhs /. T2t⋃{QU->CU}, ℏ->0]-lhs] // HL
}] // Timing

Verifying σ, m, S, and Δ.

Verifying (Subscript[σ, i->j,k->l]):

CU@(Subscript[x, 1])+CU@(Subscript[x, 2]) // (Subscript[σ, 1->3,2->4])

Verifying relabeling using m:

(Subscript[t, 1])(Subscript[t, 3])CU[(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 2])]+(Subscript[t, 1])(Subscript[t, 1])CU[(Subscript[y, 1]),(Subscript[a, 2]),(Subscript[x, 2])] // (Subscript[m, 1->3])

Verifying the meta-associativity of m:

Module[{z,u},
Table[u=CU[(Subscript[z[[1]], 1]),(Subscript[z[[2]], 2]),(Subscript[z[[3]], 3])];HL[(Subscript[m, 1,3->3])@(Subscript[m, 2,3->3])@u==(Subscript[m, 2,3->3])@(Subscript[m, 1,2->2])@u],
{z,Tuples[{y,a,x},3]},  {U,{CU,QU}}]]

Verifying the involutivity of S on CU on products of triples:

With[{bas=CU/@{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}},
Table[HL@Simp[z1**z2**z3-(Subscript[S, 1])@(Subscript[S, 1])[z1**z2**z3]],
{z1,bas},{z2,bas},{z3,bas} ] ]

Verifying that S is an anti-homomorphism on CU/QU:

With[{bas=U/@{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}},
Table[HL@Simp[(Subscript[S, 1])[z1**z2]-(Subscript[S, 1])[z2]**(Subscript[S, 1])[z1]],
{z1,bas},{z2,bas} , {U,{CU,QU}}] ]

Verifying the co-associativity of Δ:

Block[{bas=U/@{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}},
Table[(z1**z2**z3//(Subscript[Δ, 1->1,2])//(Subscript[Δ, 2->2,3]))-(z1**z2**z3//(Subscript[Δ, 1->1,3])//(Subscript[Δ, 1->1,2])) // Simp // HL,
{z1,bas},{z2,bas},{z3,bas} ,{U,{CU,QU}}] ]

Verifying S-Δ compatibility:

Block[{bas=U/@{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}},
Table[z1**z2**z3 // (Subscript[Δ, 1->1,2])//(Subscript[S, i])//(Subscript[m, 1,2->1])// Simp // HL,
{U,{CU,QU}}, {i,2}, {z1,bas},{z2,bas},{z3,bas}] ]

Verifying S-Δ compatibility for opposite m, only for CU:

Block[{bas=CU/@{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}},
Table[z1**z2**z3 // (Subscript[Δ, 1->1,2])//(Subscript[S, i])//(Subscript[m, 2,1->1])// Simp // HL,
{i,2},{z1,bas},{z2,bas},{z3,bas} ]]

Verifying m-Δ compatibility:

Block[{bas1=U/@{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, bas2=U/@{(Subscript[y, 2]),(Subscript[a, 2]),(Subscript[x, 2])}},
Table[(z1**z2**z3**z4 //(Subscript[m, 1,2->1])//(Subscript[Δ, 1->1,2])) - (z1**z2**z3**z4 // (Subscript[Δ, 1->3,4])//(Subscript[Δ, 2->5,6])//(Subscript[m, 3,5->1])//(Subscript[m, 4,6->2]))// Simp // HL,
{U,{CU,QU}},{z1,bas1},{z2,bas1},{z3,bas2},{z4,bas2} ] ]

Implementing θ

Verifying involutivity on CU:

With[{bas=CU/@{y,a,x}},
Table[z->Cθ[z]->HL[Cθ[Cθ[z]]], {z,bas}] ]

Verifying that θ is a multiplicative homomorphism on CU:

With[{bas=CU/@{y,a,x}},
Table[Cθ[z1**z2]-Cθ[z1]**Cθ[z2] // HL, {z1,bas},{z2,bas}] ]

Verifying involutivity on QU:

With[{bas=QU/@{y,a,x}},
Table[z->Qθ[z]->HL[Simp[Qθ[Qθ[z]],PowerExpand]], {z,bas}] ]

Verifying that θ is a multiplicative homomorphism on QU:

With[{bas=QU/@{y,a,x}},
Table[{z1,z2}->HL[Simp[Qθ[z1**z2]-Qθ[z1]**Qθ[z2]]], {z1,bas},{z2,bas}] ]

The Asymmetric Dequantizator

Following pensieve://People/VanDerVeen/Dequant1.pdf.

Docility of A𝔻$f:

HL@DQ@Block[{$p=4}, Collect[SS@A𝔻$f /. ω->(Subscript[a, 1]), ϵ]]

Scaling behaviour of A𝔻$f:

HL@Simplify[A𝔻$f == ((A𝔻$f /. γ->1) /. {ϵ->γ ϵ, a->(γ^(-1))a, ω->(γ^(-1))ω})]

HL@FullSimplify[A𝔻$f == ((A𝔻$f /. γ->1) /. {ℏ -> (γ^2)ℏ,ϵ->ϵ/γ, a->a/γ, t->(γ^(-2))t, ω->(γ^(-3))ω})]

Verifying that the asymmetric dequantizator is a homomorphism:

With[{bas=QU/@{y,a,x}},Table[{z1,z2}->HL[SimpT[A𝔻[z1**z2]-A𝔻[z1]**A𝔻[z2]]], {z1,bas},{z2,bas}] ]

The Symmetric Dequantizator

Following pensieve://People/VanDerVeen/Dequant1.pdf.

Verify agreement with the formulas in pensieve://People/VanDerVeen/Dequant1.pdf:

{S𝔻$P=((Cosh[ℏ(((ϵ-t)/2)+ϵ a)]-Cosh[ℏ(Sqrt[(((t^2)+(ϵ^2))/4)+ϵ ϖ])])/(ℏ Sinh[((-ϵ ℏ)/2)](ϖ-ϵ (a^2)+(t-ϵ)a+t/2))),
Simplify[S𝔻$P == (S𝔻$P /. {a->-a-1, t->-t})] // HL,
PowerExpand@Simplify[(S𝔻$P/.{ℏ -> (γ^2)ℏ,ϵ->ϵ/γ, a->a/γ, t->(γ^(-2))t, ϖ->(γ^(-3))ϖ}) == S𝔻$g(S𝔻$g /. {a->-a-γ, t->-t})] // HL,
S𝔻$Q=Simplify[S𝔻$P /. {a->c-1/2}],
Simplify[S𝔻$Q==(S𝔻$Q /. {c->-c, t->-t})] // HL,
FullSimplify[S𝔻$g==FullSimplify[(Sqrt[S𝔻$Q]) /. c->a+1/2/.{ℏ -> (γ^2)ℏ,ϵ->ϵ/γ, a->a/γ, t->(γ^(-2))t, ϖ->(γ^(-3))ϖ}]] // HL,
HL@DQ@Block[{$p=4}, Collect[SS@S𝔻$g /. ω->(Subscript[a, 1]), ϵ]],
HL@DQ@Block[{$p=4}, Collect[SS@S𝔻$f /. ω->(Subscript[a, 1]), ϵ]]
}

Verifying the θ-symmetry:

Table[HL@SimpT[Cθ[S𝔻[z]]==S𝔻[Qθ[z]]], {z, QU/@{y,a,x}}]

Verifying that the symmetric dequantizator is a homomorphism:

With[{bas=QU/@{y,a,x}},Table[{z1,z2}->HL@SimpT[S𝔻[z1**z2]-S𝔻[z1]**S𝔻[z2]], {z1,bas},{z2,bas}] ]

The representation ρ

Verifying that ρ represents CU and QU:

Table[HL[SS[ρ[z1**z2]==ρ[z1].ρ[z2]]/. (ϵ^(k_.))/;k>$k->0], {U,{CU,QU}},{z1,U/@{y,a,x}},{z2,U/@{y,a,x}} ]

Commuting (e^(α a)) with (e^(ξ x)):

Table[HL[ρ[(E^(ξ U@x))].ρ[(E^(α U@a))]==ρ[(E^(α U@a))].ρ[(E^((E^(-γ α))ξ U@x))]], {U,{CU,QU}}]

Œ and the logoi Λ

Logoi from Pensieve://Talks/Toulouse-1705/DogmaDemo.nb and from Pensieve://Talks/Sydney-1708/ExtraDetails@@.nb.

Table[
{(Subscript[Λ, U,1])[{α,β},{u,u}], lhs=U@(Subscript[Œ, U])[{(Subscript[u, 1]),(Subscript[u, 2])},ℏ(α (Subscript[u, 1])+β (Subscript[u, 2])),1], HL[lhs==U@(Subscript[Λ, U,1])[ℏ{α,β},{u,u}]]},
{U,{CU,QU}}, {u,{y,a,x}}]

{(Subscript[Λ, #,1])[{ξ,α},{x,a}], lhs=#@(Subscript[Œ, #])[{x,a},ℏ(ξ x+α a),1], HL[lhs==#@(Subscript[Λ, #,1])[ℏ{ξ,α},{x,a}]]}& /@ {CU,QU}

{(Subscript[Λ, #,2])[{α,η},{a,y}], lhs=#@(Subscript[Œ, #])[{a,y},ℏ(η y+α a),1], HL[lhs==#@(Subscript[Λ, #,2])[ℏ{α,η},{a,y}]]}& /@ {CU,QU}

Timing@(Subscript[Λ, QU,2])[{ξ,η},{x,y}]

{(Subscript[Λ, CU,1])[{ξ,η},{x,y}], lhs=CU@(Subscript[Œ, CU])[{x,y},ℏ(ξ x+η y),1], HL[lhs==CU@(Subscript[Λ, CU,1])[ℏ{ξ,η},{x,y}]]}

{(Subscript[Λ, QU,1])[{ξ,η},{x,y}], lhs=QU@(Subscript[Œ, QU])[{x,y},ℏ(ξ x+η y),1], HL@SimpT[lhs==QU@(Subscript[Λ, QU,1])[ℏ{ξ,η},{x,y}]]}

{tt=Last[(Subscript[Λ, CU,2])[{ξ,η},{x,y}]],Log[tt], Exponent[Normal@Log[tt]/.{ξ->ℏ ξ, η->ℏ η, x->ℏ x, y->ℏ y},ℏ]} // Expand

{tt=Last[(Subscript[Λ, QU,2])[{ξ,η},{x,y}]],Log[tt], Exponent[Normal@Log[tt]/.{ξ->d ξ, η->d η, x->d x, y->d y},d]} // Expand

Block[{$p=4, $k=1},
{(Subscript[Λ, CU,$k])[ℏ{ξ,η,δ},{x,y}],
Short[lhs=CU@(Subscript[Œ, CU])[{x,y},ℏ(ξ x+η y+δ x y),(Subscript[1, $k])], 5],
 HL@Simp[lhs-CU@(Subscript[Λ, CU,$k])[ℏ{ξ,η,δ},{x,y}]]}
]

{(Subscript[Λ, QU,2])[{ξ,η,δ},{x,y}], lhs=QU@(Subscript[Œ, QU])[{x,y},ℏ(ξ x+η y+δ x y),1],HL@SimpT[lhs==QU@(Subscript[Λ, QU,1])[ℏ{ξ,η,δ},{x,y}]]}

{tt=ComposeSeries[(1+t δ)Last[(Subscript[Λ, CU,2])[{ξ,η,δ},{x,y}]],(((1+t δ))^4)ϵ+((O[ϵ])^18)];Together@Log[tt],
Exponent[Normal@Together@Log[tt]/.{ξ->d ξ, η->d η, x->d x, y->d y},d],
Exponent[Normal@Together@Log[tt]/.{x->d x, y->d y},d]
} // Expand

{tt=Last[(Subscript[Λ, QU,2])[{ξ,η,δ},{x,y}]];Log[tt], Exponent[Normal@Together@Log[tt]/.{ξ->d ξ, η->d η, x->d x, y->d y},d]} // Expand

Reorderings with Rord

With[{c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[x, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2]),ℏ (Subscript[t, 1])(Subscript[a, 2])+ℏ (Subscript[t, 1]^(-1))((E^(Subscript[t, 1]))-1)(Subscript[y, 1])(Subscript[x, 2]),(Subscript[1, 2])+ϵ (Subscript[x, 1])(Subscript[y, 2])]},
{Short[rhs=c𝕠//(Subscript[Rord, (Subscript[x, 2]),(Subscript[a, 2])->3]),3], HL[CU[c𝕠]==CU[rhs]]}]

With[{c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[a, 2])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[x, 1]),(Subscript[y, 2])}, 2]),
ℏ((Subscript[l, 11])(Subscript[t, 1])(Subscript[a, 1])+(Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 21])(Subscript[t, 2])(Subscript[a, 1])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 2])+ϵ((Subscript[l, 1])(Subscript[a, 1])+(Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
{Short[rhs=c𝕠//(Subscript[Rord, (Subscript[a, 1]),(Subscript[a, 2])->3]) // (Subscript[Rord, (Subscript[x, 2]),(Subscript[x, 1])->4]),3], HL[CU[c𝕠]==CU[rhs]]}]

ℏ (Subscript[a, 3]) (Subscript[l, 11]) (Subscript[t, 1])+ℏ (Subscript[a, 3]) (Subscript[l, 12]) (Subscript[t, 1])+ℏ (Subscript[a, 3]) (Subscript[l, 21]) (Subscript[t, 2])+ℏ (Subscript[a, 3]) (Subscript[l, 22]) (Subscript[t, 2])+ℏ (Subscript[x, 4]) (Subscript[y, 1]) (Subscript[γ, 11])+ℏ (Subscript[x, 4]) (Subscript[y, 2]) (Subscript[γ, 12])+ℏ (Subscript[x, 4]) (Subscript[y, 1]) (Subscript[γ, 21])+ℏ (Subscript[x, 4]) (Subscript[y, 2]) (Subscript[γ, 22]) // Simplify

With[{c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2]),
ℏ((Subscript[l, 11])(Subscript[t, 1])(Subscript[a, 1])+(Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 21])(Subscript[t, 2])(Subscript[a, 1])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 2])+ϵ((Subscript[l, 1])(Subscript[a, 1])+(Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
{Short[rhs=c𝕠//(Subscript[Rord, (Subscript[x, 2]),(Subscript[a, 2])->3]),3], HL[CU[c𝕠]==CU[rhs]]}]

With[{q𝕠=(Subscript[Œ, QU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2]),
ℏ((Subscript[l, 11])(Subscript[t, 1])(Subscript[a, 1])+(Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 21])(Subscript[t, 2])(Subscript[a, 1])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 2])+ϵ((Subscript[l, 1])(Subscript[a, 1])+(Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
{Short[rhs=q𝕠//(Subscript[Rord, (Subscript[x, 2]),(Subscript[a, 2])->3]),3], HL[QU[q𝕠]==QU[rhs]]}]

With[{q𝕠=(Subscript[Œ, QU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2]),
ℏ((Subscript[l, 11])(Subscript[t, 1])(Subscript[a, 1])+(Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 21])(Subscript[t, 2])(Subscript[a, 1])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 2])+ϵ((Subscript[l, 1])(Subscript[a, 1])+(Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
{Short[rhs=q𝕠//(Subscript[Rord, (Subscript[a, 2]),(Subscript[y, 2])->3]),3], HL[QU[q𝕠]==QU[rhs]]}]

Timing@With[{q𝕠=(Subscript[Œ, QU])[(Subscript[{(Subscript[x, 1]),(Subscript[y, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2]),
ℏ((Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[0, 2])+ϵ((Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
{Short[rhs=q𝕠//(Subscript[Rord, (Subscript[x, 1]),(Subscript[y, 1])->3]),5]}]

Timing@With[{q𝕠=(Subscript[Œ, QU])[(Subscript[{(Subscript[x, 1]),(Subscript[y, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2]),
ℏ((Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 2])+ϵ((Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
{Short[rhs=q𝕠//(Subscript[Rord, (Subscript[x, 1]),(Subscript[y, 1])->3]),5], HL@SimpT[QU[q𝕠]==QU[rhs]]}]

Timing@With[{q𝕠=(Subscript[Œ, QU])[(Subscript[{(Subscript[x, 1]),(Subscript[y, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2]),
ℏ((Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 2])+ϵ((Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
{Short[rhs=q𝕠//(Subscript[Rord, (Subscript[x, 1]),(Subscript[y, 1])->1]),5], HL@SimpT[QU[q𝕠]==QU[rhs]]}]

Canonical ordering with Cord

Cord@(Subscript[Œ, CU])[(Subscript[{(Subscript[x, 1]),(Subscript[y, 1])}, 1]),0,(Subscript[0, 1])+(Subscript[x, 1])(Subscript[y, 1])]

Block[{$p=4,$k=0, c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 1]),
ℏ((Subscript[l, 11])(Subscript[t, 1])(Subscript[a, 1])+(Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 21])(Subscript[t, 2])(Subscript[a, 1])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 0])+ϵ((Subscript[l, 1])(Subscript[a, 1])+(Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
Timing@{Short[Cord[c𝕠],8], HL@Simp[CU[c𝕠]-CU[Cord[c𝕠]]]}]

Block[{$p=4,$k=1, c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 1]),
ℏ((Subscript[l, 11])(Subscript[t, 1])(Subscript[a, 1])+(Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 21])(Subscript[t, 2])(Subscript[a, 1])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 1])+ϵ((Subscript[l, 1])(Subscript[a, 1])+(Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
Timing@{Short[Cord[c𝕠],8], HL@Simp[CU[c𝕠]-CU[Cord[c𝕠]]]}]

With[{q𝕠=(Subscript[Œ, QU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 1]),
ℏ((Subscript[l, 11])(Subscript[t, 1])(Subscript[a, 1])+(Subscript[l, 12])(Subscript[t, 1])(Subscript[a, 2])+(Subscript[l, 21])(Subscript[t, 2])(Subscript[a, 1])+(Subscript[l, 22])(Subscript[t, 2])(Subscript[a, 2])+(Subscript[γ, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[γ, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[γ, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[γ, 22])(Subscript[x, 2])(Subscript[y, 2])),(Subscript[1, 0])+ϵ((Subscript[l, 1])(Subscript[a, 1])+(Subscript[l, 2])(Subscript[a, 2])+(Subscript[p, 11])(Subscript[x, 1])(Subscript[y, 1])+(Subscript[p, 12])(Subscript[x, 1])(Subscript[y, 2])+(Subscript[p, 21])(Subscript[x, 2])(Subscript[y, 1])+(Subscript[p, 22])(Subscript[x, 2])(Subscript[y, 2]))]},
Cord[q𝕠]]

Stitching Œ’s.

c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),(Subscript[{(Subscript[y, 2]),(Subscript[a, 2]),(Subscript[x, 2])}, 2]),(Subscript[{(Subscript[y, 3]),(Subscript[a, 3]),(Subscript[x, 3])}, 3]),ℏ Sum[(Subscript[l, 10i+j])(Subscript[t, i])(Subscript[a, j])+(Subscript[γ, 10i+j])(Subscript[y, i])(Subscript[x, j]), {i,3},{j,3}], (Subscript[1, 2])];
{c𝕠 // (Subscript[m, 3->4]), HL@Simp[CU[(Subscript[m, 3->4])[c𝕠]]-(Subscript[m, 3->4])[CU[c𝕠]]]}

Verifying that m commutes with evaluation, in CU:

c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),(Subscript[{(Subscript[y, 2]),(Subscript[a, 2]),(Subscript[x, 2])}, 2]),(Subscript[{(Subscript[y, 3]),(Subscript[a, 3]),(Subscript[x, 3])}, 3]),ℏ Sum[(Subscript[l, 10i+j])(Subscript[t, i])(Subscript[a, j])+(Subscript[γ, 10i+j])(Subscript[y, i])(Subscript[x, j]), {i,3},{j,3}], (Subscript[1, 2])];
Timing@{c𝕠 // (Subscript[m, 2->3]), HL@Simp[CU[(Subscript[m, 2->3])[c𝕠]]-(Subscript[m, 2->3])[CU[c𝕠]]]}

Verifying that m commutes with evaluation, in QU:

q𝕠=(Subscript[Œ, QU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),(Subscript[{(Subscript[y, 2]),(Subscript[a, 2]),(Subscript[x, 2])}, 2]),(Subscript[{(Subscript[y, 3]),(Subscript[a, 3]),(Subscript[x, 3])}, 3]),ℏ Sum[(Subscript[l, 10i+j])(Subscript[t, i])(Subscript[a, j])+(Subscript[γ, 10i+j])(Subscript[y, i])(Subscript[x, j]), {i,3},{j,3}], (Subscript[1, 2])];
Timing@{q𝕠 // (Subscript[m, 2->3]), HL@SimpT[QU[(Subscript[m, 2->3])[q𝕠]]-(Subscript[m, 2->3])[QU[q𝕠]]]}

Verifying meta-associativity in CU:

c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),(Subscript[{(Subscript[y, 2]),(Subscript[a, 2]),(Subscript[x, 2])}, 2]),(Subscript[{(Subscript[y, 3]),(Subscript[a, 3]),(Subscript[x, 3])}, 3]),ℏ Sum[(Subscript[λ, 10i+j])(Subscript[t, i])(Subscript[a, j])+(Subscript[γ, 10i+j])(Subscript[y, i])(Subscript[x, j]), {i,3},{j,3}], (Subscript[1, 0])];
Timing@HL[(lhs=c𝕠//(Subscript[m, 1,2->1])//(Subscript[m, 1,3->1]))≡(rhs=c𝕠//(Subscript[m, 2,3->2])//(Subscript[m, 1,2->1]))]

c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),(Subscript[{(Subscript[y, 2]),(Subscript[a, 2]),(Subscript[x, 2])}, 2]),(Subscript[{(Subscript[y, 3]),(Subscript[a, 3]),(Subscript[x, 3])}, 3]),ℏ Sum[(Subscript[λ, 10i+j])(Subscript[t, i])(Subscript[a, j])+(Subscript[γ, 10i+j])(Subscript[y, i])(Subscript[x, j]), {i,3},{j,3}], (Subscript[1, 1])];
Timing@HL[(lhs=c𝕠//(Subscript[m, 1,2->1])//(Subscript[m, 1,3->1]))≡(rhs=c𝕠//(Subscript[m, 2,3->2])//(Subscript[m, 1,2->1]))]

c𝕠=(Subscript[Œ, CU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),(Subscript[{(Subscript[y, 2]),(Subscript[a, 2]),(Subscript[x, 2])}, 2]),ℏ Sum[(Subscript[l, 10i+j])(Subscript[t, i])(Subscript[a, j])+(Subscript[γ, 10i+j])(Subscript[y, i])(Subscript[x, j]), {i,2},{j,2}], (Subscript[1, 1])];
Short[Simplify /@ (cexample=c𝕠//(Subscript[m, 1->2])), 12]
Short[Simplify /@ (qexample=(q𝕠=c𝕠 /. CU->QU)//(Subscript[m, 1->2])),12]

R in QU.

Table[Series[(Subscript[E, (Subscript[q, ℏ]),k])[x],{ϵ,0,4}], {k,0,5}] // Column

Table[Together@SeriesCoefficient[(Subscript[E, q,5])[x], {x,0,n}], {n,0,5}]

Table[HL@FunctionExpand[QFactorial[n,q]SeriesCoefficient[(Subscript[E, q,5])[x], {x,0,n}]], {n,0,5}]

QU[(Subscript[R, 3,4])] // Short

Verifying R2 (~2 secs @ $p=4, $k=2):

QU[(Subscript[R, 1,2])**(Subscript[R, 1,2]^(-1))] // Simp // HL // Timing

Verifying R3 (~156 secs @ $p=4, $k=2):

{Short[lhs=QU[(Subscript[R, 1,2])**(Subscript[R, 1,3])**(Subscript[R, 2,3])]], HL@SimpT[lhs-QU[(Subscript[R, 2,3])**(Subscript[R, 1,3])**(Subscript[R, 1,2])]]} // Timing

R in (Subscript[Œ, QU]).

{(Subscript[Œ, QU,1])[(Subscript[R, 1,2])], (Subscript[Œ, QU,2])[(Subscript[R, 1,2])]}

The morphism (Subscript[Œ, U,k]).

(Subscript[Œ, QU,1])[(Subscript[R, 1,2])(Subscript[R, 3,4])(Subscript[R, 5,6])]

(Subscript[Œ, QU,1])[(Subscript[R, 1,2])(Subscript[R, 3,4])(Subscript[R, 5,6])//(Subscript[m, 1,3->1])//(Subscript[m, 2,5->2])//(Subscript[m, 4,6->4])]

(Subscript[Œ, QU,1])[(Subscript[R, 1,2])(Subscript[R, 3,4])(Subscript[R, 5,6])//(Subscript[m, 3,1->1])//(Subscript[m, 5,2->2])//(Subscript[m, 6,4->4])]

(Subscript[Œ, QU,1])[(Subscript[R, 1,2])(Subscript[R, 3,4])(Subscript[R, 5,6])//(Subscript[m, 1,3->1])//(Subscript[m, 2,5->2])//(Subscript[m, 4,6->4])]≡(Subscript[Œ, QU,1])[(Subscript[R, 1,2])(Subscript[R, 3,4])(Subscript[R, 5,6])//(Subscript[m, 3,1->1])//(Subscript[m, 5,2->2])//(Subscript[m, 6,4->4])]

Exponentials as needed.

Block[{$p=2,$k=2},TableForm[StringSplit[
"y|a|x|Cθ@(Subscript[y, CU])|Cθ@(Subscript[a, CU])|Cθ@(Subscript[x, CU])|Qθ@(Subscript[y, QU])|Qθ@(Subscript[a, QU])|Qθ@(Subscript[x, QU])|A𝔻@(Subscript[y, QU])|A𝔻@(Subscript[a, QU])|A𝔻@(Subscript[x, QU])|S𝔻@(Subscript[y, QU])|S𝔻@(Subscript[a, QU])|S𝔻@(Subscript[x, QU])|S@(Subscript[y, CU])|S@(Subscript[a, CU])|S@(Subscript[x, CU])|S@(Subscript[y, QU])|S@(Subscript[a, QU])|S@(Subscript[x, QU])|Δ@(Subscript[y, CU])|Δ@(Subscript[a, CU])|Δ@(Subscript[x, CU])|Δ@(Subscript[y, QU])|Δ@(Subscript[a, QU])|Δ@(Subscript[x, QU])", "|"] /. s_String :> {s, Normal@Simplify@Series[ToExpression[s]/.CU|QU->Times,{ϵ,0,$k}]}]]

Timing@Block[{$p=4,$k=2},{
s=(Subscript[S, 1])[QU[(Subscript[y, 1])]] /.QU->Times,
exps=(Subscript[Exp, (Subscript[QU, 1]),$k])[η,s], (* Warning: wrong unless $p≥$k+1! *)
HL@Simp[(Subscript[S, 1])@(Subscript[𝕆, QU])[(Subscript[{(Subscript[y, 1])}, 1]),SS[(E^(ℏ η (Subscript[y, 1])))]] - QU@(exps/.η->ℏ η)]
}]

Timing@Block[{$p=4,$k=2},{
s=(Subscript[S, 1])[QU[(Subscript[a, 1])]] /.QU->Times,
exps=(Subscript[Exp, (Subscript[QU, 1]),$k])[α,s], (* Warning: wrong unless $p≥$k+1! *)
HL@Simp[(Subscript[S, 1])@(Subscript[𝕆, QU])[(Subscript[{(Subscript[a, 1])}, 1]),SS[(E^(ℏ α (Subscript[a, 1])))]] - QU@(exps/.α->ℏ α)]
}]

Timing@Block[{$p=4,$k=2},{
s=(Subscript[S, 1])[QU[(Subscript[x, 1])]] /.QU->Times,
exps=(Subscript[Exp, (Subscript[QU, 1]),$k])[ξ,s], (* Warning: wrong unless $p≥$k+1! *)
HL@Simp[(Subscript[S, 1])@(Subscript[𝕆, QU])[(Subscript[{(Subscript[x, 1])}, 1]),SS[(E^(ℏ ξ (Subscript[x, 1])))]] - QU@(exps/.ξ->ℏ ξ)]
}]

S((e^(η y))(e^(α a))(e^(ξ x)))

Timing@Block[{$p=3,$k=1},{
(sexp=(Subscript[m, 3,2,1->1])[(Subscript[Exp, (Subscript[QU, 1]),$k])[η,(Subscript[S, 1])[QU[(Subscript[y, 1])]]/.QU->Times](Subscript[Exp, (Subscript[QU, 2]),$k])[α,(Subscript[S, 2])[QU[(Subscript[a, 2])]]/.QU->Times](Subscript[Exp, (Subscript[QU, 3]),$k])[ξ,(Subscript[S, 3])[QU[(Subscript[x, 3])]]/.QU->Times]]) /. (Subscript[u_, 1]):>u,
HL@SimpT[QU@(sexp /. {η->ℏ η, α->ℏ α, ξ->ℏ ξ})- (Subscript[S, 1])@(Subscript[𝕆, QU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),SS[(E^(ℏ(η (Subscript[y, 1])+α (Subscript[a, 1])+ξ (Subscript[x, 1]))))]]]
}]

(Subscript[Δ, 1->1,2])((e^(η (Subscript[y, 1])))(e^(α (Subscript[a, 1])))(e^(ξ (Subscript[x, 1]))))

Timing@Block[{$p=4,$k=2},{
sexp=(Subscript[m, 1,3,5->1])@(Subscript[m, 2,4,6->2])@Times[ (* Warning: wrong unless $p≥$k+1! *)
Prepend[(Subscript[{(Subscript[y, 2])}, 2])]@(Subscript[Exp, (Subscript[QU, 1]),$k])[η,(Subscript[Δ, 1->1,2])[QU[(Subscript[y, 1])]]/.QU->Times],
Prepend[(Subscript[{(Subscript[a, 4])}, 4])]@(Subscript[Exp, (Subscript[QU, 3]),$k])[α,(Subscript[Δ, 3->3,4])[QU[(Subscript[a, 3])]]/.QU->Times],
Prepend[(Subscript[{(Subscript[x, 6])}, 6])]@(Subscript[Exp, (Subscript[QU, 5]),$k])[ξ,(Subscript[Δ, 5->5,6])[QU[(Subscript[x, 5])]]/.QU->Times]
] /. {η->ℏ η, α->ℏ α, ξ->ℏ ξ},
HL@SimpT[QU@sexp - (Subscript[Δ, 1->1,2])@(Subscript[𝕆, QU])[(Subscript[{(Subscript[y, 1]),(Subscript[a, 1]),(Subscript[x, 1])}, 1]),SS[(E^(ℏ(η (Subscript[y, 1])+α (Subscript[a, 1])+ξ (Subscript[x, 1]))))]]]
}]

Zip and Bind

QZip implements the “Q-level zips” on 𝔼(L,Q,P)=((Pe)^(L+Q)). Such zips regard the L variables as scalars.

Timing@{E0=𝔼[0,Sum[(Subscript[a, 10i+j])(Subscript[x, i])(Subscript[ξ, j]),{i,3},{j,3}],1+ϵ Sum[(Subscript[f, i])[(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[x, 3])](Subscript[ξ, i]),{i,3}]+ϵ Sum[(Subscript[f, 10i+j])[(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[x, 3])](Subscript[ξ, i])(Subscript[ξ, j]),{i,3},{j,3}]],
lhs=(Subscript[QZip, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E0,
HL[lhs==(Subscript[QZip, {(Subscript[ξ, 1])}])@(Subscript[QZip, {(Subscript[ξ, 2])}])@E0]}

Timing@{
Eh=𝔼[0,h Sum[(Subscript[a, 10i+j])(Subscript[x, i])(Subscript[ξ, j]),{i,3},{j,3}],1+ϵ Sum[(Subscript[f, i])[(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[x, 3])](Subscript[ξ, i]),{i,3}]+ϵ Sum[(Subscript[f, 10i+j])[(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[x, 3])](Subscript[ξ, i])(Subscript[ξ, j]),{i,3},{j,3}]],
lhs=Normal[Eh /. 𝔼[L_,Q_,P_] :> Series[P (E^(L+Q)),{h,0,2}]] // (Subscript[Zip, {(Subscript[ξ, 1])}]),
HL@Simplify[lhs==Normal[(Subscript[QZip, {(Subscript[ξ, 1])}])[Eh]/. 𝔼[L_,Q_,P_] :> Series[P (E^(L+Q)),{h,0,2}]]]}

LZip implements the “L-level zips” on 𝔼(L,Q,P)=((Pe)^(L+Q)). Such zips regard all of ((Pe)^Q) as a single”P”. Here the z’s are t and α and the ζ’s are τ and a.

(Subscript[Bind, {2}])[𝔼[0,ξ((Subscript[x, 1])+(Subscript[x, 2])),1],𝔼[0,(Subscript[ξ, 2])((Subscript[x, 2])+(Subscript[x, 3])),1]]

(Subscript[Bind, {2}])[𝔼[0,((Subscript[ξ, 2])+(Subscript[ξ, 3]))(Subscript[x, 2]),1],𝔼[0,((Subscript[ξ, 1])+(Subscript[ξ, 2]))x,1]]

(Subscript[Bind, {1,2}])[𝔼[0,((Subscript[ξ, 2])+(Subscript[ξ, 3]))(Subscript[x, 2])+(Subscript[ξ, 1])(Subscript[x, 1]),1],𝔼[0,((Subscript[ξ, 1])+(Subscript[ξ, 2]))x,1]]

An xay->axy->ayx->yax≡xay->xya->yxa->yax test:

Bind[𝔼[(Subscript[α, 1]) (Subscript[a, 1])+(Subscript[τ, 1])(Subscript[t, 1]),(E^(γ (Subscript[α, 1])))(Subscript[ξ, 1]) (Subscript[x, 1])+(Subscript[η, 1])(Subscript[y, 1]),1],{1},𝔼[(Subscript[τ, 1])(Subscript[t, 1])+(Subscript[α, 1])(Subscript[a, 1]),(Subscript[ξ, 1])(Subscript[x, 1])+(Subscript[η, 1])(Subscript[y, 1])+(Subscript[ξ, 1])(Subscript[η, 1])(Subscript[t, 1]),1]]

Column@{Cord[(Subscript[Œ, CU])[(Subscript[{(Subscript[x, 1]),(Subscript[a, 1])}, 1]),(Subscript[ξ, 1])(Subscript[x, 1])+(Subscript[α, 1])(Subscript[a, 1]),1+(Subscript[0, 0])]],
Cord[(Subscript[Œ, CU])[(Subscript[{(Subscript[x, 1]),(Subscript[y, 1])}, 1]),(Subscript[ξ, 1])(Subscript[x, 1])+(Subscript[η, 1])(Subscript[y, 1]),1+(Subscript[0, 0])]],
Cord[(Subscript[Œ, CU])[(Subscript[{(Subscript[a, 1]),(Subscript[y, 1])}, 1]),(Subscript[α, 1])(Subscript[a, 1])+(Subscript[η, 1])(Subscript[y, 1]),1+(Subscript[0, 0])]]}

{rxa=𝔼[(Subscript[τ, 1])(Subscript[t, 1])+(Subscript[α, 1])(Subscript[a, 1]),(E^(-γ (Subscript[α, 1])))(Subscript[ξ, 1]) (Subscript[x, 1])+(Subscript[η, 1])(Subscript[y, 1]),1];
rxy=𝔼[(Subscript[τ, 1])(Subscript[t, 1])+(Subscript[α, 1])(Subscript[a, 1]),(Subscript[ξ, 1])(Subscript[x, 1])+(Subscript[η, 1])(Subscript[y, 1])-(Subscript[ξ, 1])(Subscript[η, 1])(Subscript[t, 1]),1];
ray=𝔼[(Subscript[τ, 1])(Subscript[t, 1])+(Subscript[α, 1])(Subscript[a, 1]),(E^(-γ (Subscript[α, 1])))(Subscript[η, 1]) (Subscript[y, 1])+(Subscript[ξ, 1])(Subscript[x, 1]),1];
lhs=Expand /@ Bind[rxa,{1},rxy,{1},ray],
HL[lhs==Expand /@ Bind[ray,{1},rxy,{1},rxa] ]}

Simplify/@(Subscript[m, i,j->k])@(Subscript[Œ, CU])[(Subscript[{(Subscript[y, i]),(Subscript[a, i]),(Subscript[x, i])}, i]),(Subscript[{(Subscript[y, j]),(Subscript[a, j]),(Subscript[x, j])}, j]),(Subscript[η, i])(Subscript[y, i])+(Subscript[α, i])(Subscript[a, i])+(Subscript[ξ, i])(Subscript[x, i])+(Subscript[η, j])(Subscript[y, j])+(Subscript[α, j])(Subscript[a, j])+(Subscript[ξ, j])(Subscript[x, j]),1+(Subscript[0, 1])]

Tensorial Representations

Associativity of tm.

Table[Block[{$U=U,$k=kk},
{lhs=Bind[(Subscript[tm, 1,2->2]),{2},(Subscript[tm, 2,3->1])];
{$U,$k}->HL[lhs≡Bind[(Subscript[tm, 2,3->2]),{2},(Subscript[tm, 1,2->1])]]}
],{U,{CU,QU}},{kk,0,1}]

Block[{$U=CU,$k=2},Timing@{lhs=Bind[(Subscript[tm, 1,2->2]),{2},(Subscript[tm, 2,3->1])];HL[lhs≡Bind[(Subscript[tm, 2,3->2]),{2},(Subscript[tm, 1,2->1])]]}]

tS is an anti-homomorphism for tm.

HL[((Subscript[tS, 1])(Subscript[tS, 2]))~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])≡(Subscript[tm, 2,1->1])~(Subscript[B, 1])~(Subscript[tS, 1])]

Testing co-associativity.

HL[(Subscript[tΔ, 1->1,2])~(Subscript[B, 2])~(Subscript[tΔ, 2->2,3])≡(Subscript[tΔ, 1->1,3])~(Subscript[B, 1])~(Subscript[tΔ, 1->1,2])]

Testing S is an anti-co-homomorphism

HL[(Subscript[tS, 1])~(Subscript[B, 1])~(Subscript[tΔ, 1->1,2])≡(Subscript[tΔ, 1->2,1])~(Subscript[B, 1,2])~((Subscript[tS, 1])(Subscript[tS, 2]))]

Testing convolution inverse:

{HL[(Subscript[tΔ, 1->1,2])~(Subscript[B, 1])~(Subscript[tS, 1])~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])≡tη~(Subscript[B, {}])~t𝟙],
HL[(Subscript[tΔ, 1->1,2])~(Subscript[B, 2])~(Subscript[tS, 2])~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])≡tη~(Subscript[B, {}])~t𝟙]}

Testing R2

HL[((Subscript[(OverBar[tR]), 1,2])(Subscript[tR, 3,4]))~(Subscript[B, 1,2,3,4])~((Subscript[tm, 1,3->1])(Subscript[tm, 2,4->2]))==t𝟙]

Testing quasi-triangular axioms

HL[((Subscript[tΔ, 1->1,2])(Subscript[tR, 3,4]))~(Subscript[B, 1,2,3,4])~((Subscript[tm, 1,3->1])(Subscript[tm, 2,4->2]))≡((Subscript[tΔ, 1->2,1])(Subscript[tR, 3,4]))~(Subscript[B, 1,2,3,4])~((Subscript[tm, 3,1->1])(Subscript[tm, 4,2->2]))]

HL[(Subscript[tR, 1,3])~(Subscript[B, 1])~(Subscript[tΔ, 1->1,2])≡((Subscript[tR, 1,4])(Subscript[tR, 2,3]))~(Subscript[B, 3,4])~(Subscript[tm, 3,4->3])]

Testing R3

HL[((Subscript[tR, 2,3])(Subscript[tR, 1,4])(Subscript[tR, 5,6]))~(Subscript[B, Range@6])~((Subscript[tm, 1,5->1])(Subscript[tm, 2,6->2])(Subscript[tm, 3,4->3]) )≡((Subscript[tR, 1,2])(Subscript[tR, 5,3])(Subscript[tR, 6,4]))~(Subscript[B, Range@6])~((Subscript[tm, 1,5->1])(Subscript[tm, 2,6->2])(Subscript[tm, 3,4->3]) )]

tC is the counterclockwise spinner; (OverBar[tC]) is its inverse:

Block[{$k=1},HL[((Subscript[tC, 1])(Subscript[(OverBar[tC]), 2]))~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])≡t𝟙]]

Cyclic R2 as on 180419 blackboard:

Block[{$k=2},HL[((Subscript[tR, 1,4])(Subscript[(OverBar[tR]), 5,2])(Subscript[(OverBar[tC]), 3]))~(Subscript[B, {1,3,2,4}])~((Subscript[tm, 1,3->1]) (Subscript[tm, 2,4->2]))~(Subscript[B, 1,5])~(Subscript[tm, 1,5->1])≡(Subscript[(OverBar[tC]), 1])]]//Timing

Swirl relation as on 180419 blackboard:

Block[{$k=1},HL[(Subscript[tR, 1,2])≡((Subscript[tC, 1])(Subscript[tC, 2])(Subscript[tR, 3,4])(Subscript[(OverBar[tC]), 5])(Subscript[(OverBar[tC]), 6]))~(Subscript[B, 1,2,3,4])~((Subscript[tm, 1,3->1])(Subscript[tm, 2,4->2]))~(Subscript[B, 1,2,5,6])~((Subscript[tm, 1,5->1])(Subscript[tm, 2,6->2]))]]//Timing

The Four Kinks

Block[{$k=2,K1,K2,K3,K4},
Column@{K1=((Subscript[tR, 1,3])(Subscript[(OverBar[tC]), 2]))~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])~(Subscript[B, 1,3])~(Subscript[tm, 1,3->1]), K2=((Subscript[tR, 3,1])(Subscript[tC, 2]))~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])~(Subscript[B, 1,3])~(Subscript[tm, 1,3->1]), K3=((Subscript[(OverBar[tR]), 3,1])(Subscript[(OverBar[tC]), 2]))~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])~(Subscript[B, 1,3])~(Subscript[tm, 1,3->1]), K4=((Subscript[(OverBar[tR]), 1,3])(Subscript[tC, 2]))~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])~(Subscript[B, 1,3])~(Subscript[tm, 1,3->1]),
HL/@{
K1≡(Subscript[tKink, 1]),K3≡(Subscript[(OverBar[tKink]), 1]),
K1≡K2,K3≡K4,
(K1(K3~(Subscript[B, 1,2])~(Subscript[tm, 1,2->2])))~(Subscript[B, 1,2])~(Subscript[tm, 1,2->1])≡t𝟙,
K1~(Subscript[B, 1])~(Subscript[tS, 1])≡K1,K3~(Subscript[B, 1])~(Subscript[tS, 1])≡K3}
}]

Trefoil as on 180419 blackboard:

Timing[
Z=(Subscript[tR, 1,5])(Subscript[tR, 6,2])(Subscript[tR, 3,7])(Subscript[(OverBar[tC]), 4])(Subscript[(OverBar[tKink]), 8])(Subscript[(OverBar[tKink]), 9])(Subscript[(OverBar[tKink]), 10]);
Do[Z;Z=Z~(Subscript[B, 1,k])~(Subscript[tm, 1,k->1]),{k,2,10}];
Z]

Alternative Algorithms

{(Subscript[λ, alt,2])[CU], HL@Simplify@Normal[(Subscript[λ, alt,2])[CU]==Last[(Subscript[Λ, CU,2])[{ξ,η},{x,y}]]]}