Pensieve header: A unified verification notebook for the $sl_2$-portfolio project; continues pensieve://Projects/PPSA/nb/Verfication.pdf.

Continues pensieve://2017-06/ and pensieve://2017-08/.

Prolog

Go;

wdir=SetDirectory["C:\\drorbn\\AcademicPensieve\\Projects\\SL2Portfolio"];
NotebookOpen[wdir<>"\\MakeSnips.nb"];

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

Initialization / Utilities

The “degree carrier / filtration parameter” is ℏ, and all “coupling constants” are proportional to it.

$TℏD=3; $TϵD=2; ϵ /: (ϵ^(d_. ))/; d>$TϵD :=0;
(* $TϵD can't be ∞ at least because of Quesne. Can't be ≤1 at least because of the explicit (ϵ^2) in S𝔻$g. *)
SetAttributes[{SS, SST}, HoldAll];
SS[ℰ_] := Block[{ℏ,ϵ}, (* Shielded Series *)
Collect[Normal@Series[ℰ, {ℏ,0,$TℏD}],ℏ,Together] ];
SST[ℰ_] := Block[{ℏ,ϵ},Collect[Normal@Series[ℰ/.{(Subscript[T, i_])-> (E^(ℏ (Subscript[t, i])/2)),T-> (E^(ℏ t/2))}, {ℏ,0,$TℏD}],ℏ,Together] ];
Simp[ℰ_, op_]:= Collect[ℰ, _CU|_QU, op];
Simp[ℰ_]:=Simp[ℰ,Collect[Normal@Series[#, {ℏ,0,$TℏD}],ℏ,Expand]&];
SimpT[ℰ_]:= Collect[ℰ, _CU|_QU, Collect[Normal@Series[#/.{(Subscript[T, i_])-> (E^(ℏ (Subscript[t, i])/2)),T-> (E^(ℏ t/2))}, {ℏ,0,$TℏD}],ℏ,Expand]&];

Differential polynomials (DP):

(Subscript[DP, α_->(Subscript[D, x_]),β_->(Subscript[D, y_])])[P_][λ_]:=Total[CoefficientRules[P,{α,β}]/.({m_,n_}->c_):>c D[λ,{x,m},{y,n}]]

DeclareAlgebra

Unprotect[NonCommutativeMultiply]; Attributes[NonCommutativeMultiply]={};
(NCM=NonCommutativeMultiply)[x_] := x;
NCM[x_,y_,z__] := (x**y)**z;
0**_=_**0=0;
(x_Plus)**y_:=(#**y)&/@x; x_**(y_Plus):=(x**#)&/@y;
B[x_,x_]=0; B[x_,y_] := x**y-y**x;

DeclareAlgebra[U_Symbol, opts__Rule] := Module[{gp,sr,cp,CE,pow,
gs=Generators /. {opts}, cs=Centrals /. {opts} },
((Subscript[#, U])=U@#)&/@gs;
gp=Alternatives@@gs; gp=gp|(Subscript[gp, _]);(* gen's pattern *)
sr=Thread[gs->Range@Length@gs]; (* sorting rule *)
cp=Alternatives@@cs; (* cent's pattern *)
CE[ℰ_]:= Collect[ℰ, _U, (Expand[#] /. (ℏ^(d_))/;d>$TℏD:>0)&];
(Subscript[U, i_])[ℰ_] := ℰ /. {t:cp:>(Subscript[t, i]),u_U :> Replace[u, x_ :> (Subscript[x, i]),1]};
(Subscript[U, i_])[NCM[]]:=U[];
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[U@y_,U@x_]:=CE[-B[U@x,U@y]];
x_**U[]:=x; U[]**x_:=x;
(a_.*x_U)**(b_.*y_U) := If[a b === 0, 0, CE[a b (x**y)]];
U[xx___,x_] ** U[y_,yy___] := If[OrderedQ[{x,y}/.sr],U[xx,x,y,yy], U@xx**(U@y**U@x+B[U@x,U@y])**U@yy];
U@{c_.*(((l:gp))^(n_)),r___}/;FreeQ[c, gp]:= CE[c U@Table[l,{n}]**U@{r}];
U@{c_.*l:gp,r___} := CE[c U[l]**U@{r}];
U@{c_,r___}/;FreeQ[c, gp]:= CE[c U@{r}];
U@{}=U[];
U@{l_Plus, r___} := CE[U@{#,r}& /@ l];
U@{l_,r___} := U@{Expand[l],r};
U[ℰ_NonCommutativeMultiply]:=U/@ℰ;
(Subscript[𝕆, U])[poly_, specs___] := Module[{sp,null,vs,us},
sp=Replace[{specs}, l_List:>(Subscript[l, null]), {1}];
vs=Join@@(First /@ sp);
us=Join@@(sp /. (Subscript[l_, s_]) :> (l/.(Subscript[x_, i_]):>(Subscript[x, s])));
CE[Total[
CoefficientRules[poly, vs] /. (p_->c_) :> c U@((us^p))
]] /. (Subscript[x_, null]):>x
 ];
pow[ℰ_,0]=U[]; pow[ℰ_,n_]:=pow[ℰ,n-1]**ℰ;
(Subscript[𝕊, U])[ℰ_,ss___Rule] := CE@Total[
CoefficientRules[ℰ,First/@{ss}]/.(p_->c_):>c NCM@@MapThread[pow,{Last/@{ss},p}]];
(Subscript[S, i_])[c_.*u_U]:= CE[(c/.(Subscript[S, i])[U,Centrals])DeleteCases[u,(Subscript[_, i])]**(Subscript[U, i])[NCM@@Reverse@Cases[u,(Subscript[x_, i]):>S@U@x]]];
]

DeclareMorphism

DeclareMorphism[m_,U_->V_, ongs_List, oncs_List:{}] := (
Replace[ongs, (g_->img_) :> (m[U[g]]=img), {1}];
m[U[]]=V[];
m[U[(Subscript[g_, i_])]] := (Subscript[V, i])[m[U@g]];
m[U[vs__]] := NCM@@(m/@U/@{vs});
m[ℰ_] := Simp[ℰ /. oncs /.  u_U:>m[u]]; )

Meta-Operations

(Subscript[S, i_])[ℰ_Plus] := Simp[(Subscript[S, i])/@ℰ];

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

DeclareAlgebra[CU,Generators->{y,a,x},Centrals->{t}];
B[(Subscript[a, CU]),(Subscript[y, CU])]=-γ (Subscript[y, CU]); B[(Subscript[x, CU]),(Subscript[a, CU])]=-γ (Subscript[x, CU]);
B[(Subscript[x, CU]),(Subscript[y, CU])]=2ϵ (Subscript[a, CU])-t CU[];
(S@CU@y=-(Subscript[y, CU]); S@(Subscript[a, CU])=-(Subscript[a, CU]); S@(Subscript[x, CU])=-(Subscript[x, CU]);)
(Subscript[S, i_])[CU,Centrals]={(Subscript[t, i])->-(Subscript[t, i])};

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

Verifying that S is an anti-homomorphism on CU:

With[{bas=CU/@{(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} ] ]

Verifying the involutivity of S 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} ] ]

Implementing (Subscript[𝒰, γϵ;ℏ])

With q=(e^(ℏγϵ)), A=(e^(-ℏϵa)), T=(e^(ℏt/2)), and (Subscript[[f,g], q]):=fg-qgf, our algebra is (Subscript[𝒰, γϵ;ℏ])=⟨t,y,a,x⟩/ℛ, where ℛ=([t,*]=0, [a,y]=-γy, (Subscript[[x,y], q])=(1-(T^2)(A^2))/ℏ,[x,a]=-γx).

DeclareAlgebra[QU, Generators -> {y,a,x}, Centrals -> {t,T}];
q=SS[(E^(γ ϵ ℏ))]; (*T=SS[(E^(ℏ t/2))];*)
B[(Subscript[a, QU]),(Subscript[y, QU])]=-γ (Subscript[y, QU]); B[(Subscript[x, QU]),(Subscript[a, QU])]=-γ QU@x;
B[(Subscript[x, QU]),(Subscript[y, QU])]=(q-1)QU@{y,x}+(Subscript[𝕆, QU])[SS[(1-(T^2)(E^(-2ϵ a ℏ)))/ℏ], {a}];
(S@(Subscript[y, QU])=(Subscript[𝕆, QU])[SS[-(T^(-2))(E^(ℏ ϵ a))y],{a,y}]; S@(Subscript[a, QU])=-(Subscript[a, QU]); S@(Subscript[x, QU])=(Subscript[𝕆, QU])[SS[-(E^(ℏ ϵ a))x],{a,x}];)
(Subscript[S, i_])[QU,Centrals]={(Subscript[t, i])->-(Subscript[t, i]), (Subscript[T, i])->(Subscript[T, i]^(-1))};

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 @ $TℏD=5, $TϵD=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 S is an anti-homomorphism on QU:

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

Verifying that (Subscript[Lim, ℏ->0])QU=CU using a “random” product (~23 secs @ $TℏD=5, $TϵD=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 /. {QU->CU, T-> (E^(ℏ t/2))}, ℏ->0]-lhs] // HL
}] // Timing

Implementing θ

DeclareMorphism[Cθ,CU->CU, {y->-(Subscript[x, CU]), a->-(Subscript[a, CU]), x->-(Subscript[y, CU])}, {t->-t, T->(T^(-1))}];DeclareMorphism[Qθ,QU->QU, {y->(Subscript[𝕆, QU])[SS[-(T^(-1))(E^(ℏ ϵ a))x],{a,x}], a->-(Subscript[a, QU]), x->(Subscript[𝕆, QU])[SS[-(T^(-1))(E^(ℏ ϵ a))y],{a,y}]}, {t->-t, T->(T^(-1))}]

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[Qθ[Qθ[z]]], {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.

A𝔻$f=(γ/ℏ) (E^(ℏ((t/2)-(a+γ)ϵ)))((Cosh[ℏ(a ϵ+((γ ϵ)/2)-(t/2))]-Cosh[ℏ(Sqrt[(((((t-γ ϵ)/2)))^2)+ϵ ω])])/(Sinh[((γ ϵ ℏ)/2)]((a^2)ϵ+a γ ϵ-a t-ω)));

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))ω})]

A𝔻$ω=γ CU[y,x]+ϵ CU[a,a]-(t-γ ϵ)CU[a];

DeclareMorphism[A𝔻,QU->CU,{a->(Subscript[a, CU]),x->CU@x, y->(Subscript[𝕊, CU])[SS[A𝔻$f],a->(Subscript[a, CU]),ω->A𝔻$ω]**(Subscript[y, CU])}]

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.

S𝔻$g=(Sqrt[((Cosh[(ℏ/2)(Sqrt[(t^2)+(γ^2) (ϵ^2)+4 ϵ ϖ])]-Cosh[(ℏ/2)(t-(2 a+γ) ϵ)])/(Sinh[((γ ϵ ℏ)/2)](t (2 a+γ)-2 a (a+γ) ϵ+2 ϖ) ℏ/(2γ)))]);

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,
Simplify[S𝔻$g==FullSimplify[(Sqrt[S𝔻$Q]) /. c->a+1/2/.{ℏ -> (γ^2)ℏ,ϵ->ϵ/γ, a->a/γ, t->(γ^(-2))t, ϖ->(γ^(-3))ϖ}]] // HL
}

S𝔻$f=FullSimplify[(E^(ℏ(t/2-ϵ a)))(S𝔻$g /. {a->-a, t->-t})];

S𝔻$ϖ=γ CU[y,x]+ϵ CU[a,a]-(t-γ ϵ)CU[a]-t γ CU[]/2;

DeclareMorphism[S𝔻,QU->CU,{a->(Subscript[a, CU]),
x->(Subscript[𝕊, CU])[SS[S𝔻$f],a->(Subscript[a, CU]),ϖ->S𝔻$ϖ]**(Subscript[x, CU]),
y->(Subscript[𝕊, CU])[SS[S𝔻$g],a->(Subscript[a, CU]),ϖ->S𝔻$ϖ]**(Subscript[y, CU])
}]

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}] ]

R in QU.

Quesne’s formula:

(Subscript[E, q_,n_])[x_]:=E^((∑_(k=1)^n) (((((1-q))^k)(x^k))/(k(1-(q^k))))); (Subscript[E, q_])[x_]:=(Subscript[E, q,$TϵD])[x]

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

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

QU[(Subscript[R, i_,j_])] := (Subscript[𝕆, QU])[SS[(E^(ℏ (Subscript[b, 1])(Subscript[a, 2])))(Subscript[E, q])[ℏ (Subscript[y, 1]) (Subscript[x, 2])]/.(Subscript[b, 1])->(γ^(-1))(ϵ (Subscript[a, 1])-(Subscript[t, i]))], (Subscript[{(Subscript[y, 1]),(Subscript[a, 1])}, i]), (Subscript[{(Subscript[a, 2]),(Subscript[x, 2])}, j])];
QU[(Subscript[R, i_,j_]^(-1))] := (Subscript[S, j])@QU[(Subscript[R, i,j])];

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

Verifying R2 (~2 secs @ $TℏD=4, $TϵD=2):

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

Verifying R3 (~156 secs @ $TℏD=4, $TϵD=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

The representation ρ

ρ@(Subscript[y, CU])=ρ@(Subscript[y, QU])=(({{0, 0}, {ϵ, 0}}));ρ@(Subscript[a, CU])=ρ@(Subscript[a, QU])=(({{γ, 0}, {0, 0}}));
ρ@(Subscript[x, CU])=(({{0, γ}, {0, 0}})); ρ@(Subscript[x, QU])=SS@(({{0, (1-(E^(-γ ϵ ℏ)))/(ϵ ℏ)}, {0, 0}}));
ρ[(E^(ℰ_))]:=MatrixExp[ρ[ℰ]];
ρ[ℰ_]:=(ℰ/.{t->γ ϵ,T->(E^(ℏ γ ϵ/2))}/.(U:CU|QU)[u___]:>Fold[Dot,(({{1, 0}, {0, 1}})),ρ/@U/@{u}])

Verifying that ρ represents CU and QU:

Table[ρ[z1**z2]==ρ[z1].ρ[z2] // SS // HL,
{U,{CU,QU}},{z1,U/@{y,a,x}},{z2,U/@{y,a,x}} ]

The Classical Logos CΛ

Lemma 3C. To degree k, (Subscript[𝕆, CU])((e^(η y+ξ x+δ y x))|x y)=(Subscript[𝕆, CU])(ν (e^(ν(-t ξ η+η y+ξ x+δ y x)))(Subscript[CΛ, k])(ϵ,γ,y,a,x,η,ξ,δ)|y a x), with ν=(((1+t δ))^(-1)) and where (Subscript[CΛ, k])(ϵ,γ,y,a,x,η,ξ,δ) is a fixed polynomial of degree at most 4k in y,(Sqrt[a]),x,η,ξ, with scalar coefficients.

Comment. Even better, log((Subscript[CΛ, k])) is of degree at most 2k+2 in said variables.

eqn=ρ[(E^(ξ (Subscript[x, CU])))].ρ[(E^(η (Subscript[y, CU])))]==ρ[(E^(d (Subscript[y, CU])))].ρ[(E^(c(t CU[] - 2ϵ (Subscript[a, CU]))))].ρ[(E^(b (Subscript[x, CU])))]

sol=Solve[Thread[Flatten/@eqn], {d,b,c}][[1]]/. C[1]->0

Proof of Lemma 3C. We know that (Subscript[𝕆, CU])((e^(ξ x + η y))|x y)=(Subscript[𝕆, CU])((e^(c t + a y - 2ϵ c a + b x))|y a x), with {d->(η/(1+γ ϵ η ξ)),b->(ξ/(1+γ ϵ η ξ)),c->((Log[1+γ ϵ η ξ])/(-γ ϵ))}. Expanding in ϵ we get (Subscript[𝕆, CU])((e^(ξ x + η y))|x y)= (Subscript[𝕆, CU])((Subscript[λ, ϵ])(ξ,η)(e^(η y + ξ x - η ξ t))|y a x) = (Subscript[𝕆, CU])((Subscript[λ, ϵ])((∂_x),(∂_y))(e^(η y + ξ x - η ξ t))|y a x) and so (Subscript[𝕆, CU])((e^(η y+ξ x+δ y x))|x y)= 𝕆((Subscript[λ, ϵ])((∂_x),(∂_y))(e^(δ (∂_η)(∂_ξ)))(e^(η y + ξ x - η ξ t))|y a x) = 𝕆((Subscript[λ, ϵ])((∂_x),(∂_y))ν (e^(ν(-t ξ η+η y+ξ x+δ y x)))|y a x).

(Subscript[SS, ϵ])[ℰ_] := Block[{ϵ},Collect[Normal@Series[ℰ, {ϵ,0,$TϵD}],ϵ,Together]];  (* Shielded ϵ-Series *)
CΛ[t1_,y1_,a1_,x1_,ξ1_,η1_,δ_]:=Module[
{eqn,d,b,c,sol,λ,q,ν, ξ, η},
eqn=ρ[(E^(ξ (Subscript[x, CU])))].ρ[(E^(η (Subscript[y, CU])))]==ρ[(E^(d (Subscript[y, CU])))].ρ[(E^(c(t CU[] - 2ϵ (Subscript[a, CU]))))].ρ[(E^(b (Subscript[x, CU])))];
sol=Solve[Thread[Flatten/@eqn], {d,b,c}][[1]] /. C[1]->0;
λ=Simplify[(E^(-η y-ξ x+η ξ t))(Subscript[SS, ϵ])[(E^(c t + d y - 2ϵ c a + b x))/.sol]];
q=(E^(ν(-t ξ η+η y+ξ x+δ y x)));
Collect[ν (q^(-1))(Subscript[DP, ξ->(Subscript[D, x]),η->(Subscript[D, y])])[λ][q] /. ν->(((1+t δ))^(-1)),ϵ,Simplify] /. {t->t1,y->y1,a->a1,x->x1,ξ->ξ1, η->η1}
];

CΛ[t,y,a,x,ξ,η,δ]

{Short[lhs=(Subscript[𝕆, CU])[SS[(E^(ℏ(ξ x+η y+δ x y)))],{x,y}], 5], HL[lhs==(Subscript[𝕆, CU])[SS[(E^(ℏ ν(ξ x+η y+δ x y-t ℏ ξ η)))CΛ[t,y,a,x,ℏ ξ,ℏ η,ℏ δ] /. ν ->(((1+ℏ t  δ))^(-1))],{y,a,x}]]}

C𝕆 and Swaps

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

SetAttributes[C𝕆, Orderless];
CU@C𝕆[specs___, 𝔼[L_,Q_,P_]] := (Subscript[𝕆, CU])[SS[(E^(L+Q))P], specs]

CU@C𝕆[𝔼[ℏ (Subscript[t, 1])(Subscript[a, 2]),ℏ (Subscript[t, 1]^(-1))((E^(Subscript[t, 1]))-1)(Subscript[y, 1])(Subscript[x, 2]),1+ϵ (Subscript[x, 1])(Subscript[y, 2])], (Subscript[{(Subscript[y, 1]),(Subscript[x, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2])] // Short

HL[ρ[(E^(ξ CU@x))].ρ[(E^(α CU@a))]==ρ[(E^(α CU@a))].ρ[(E^((E^(-γ α))ξ CU@x))]]

(Subscript[SW, (Subscript[x, i_]),(Subscript[a, j_])])[C𝕆[(Subscript[{lh___,(Subscript[x, i_]),(Subscript[a, j_]),rh___}, s_]),more___,𝔼[L_,Q_,P_]]] := C𝕆[(Subscript[{lh,(Subscript[a, j]),(Subscript[x, i]),rh}, s]),more,
With[{q=(E^(-γ α))ξ (Subscript[x, i])+α (Subscript[a, j])},
𝔼[L,(E^(-γ α))ξ (Subscript[x, i])+(Q/.(Subscript[x, i])->0), (E^(-q))(Subscript[DP, (Subscript[x, i])->(Subscript[D, ξ]),(Subscript[a, j])->(Subscript[D, α])])[P][(E^q)]] /. {α->(∂_(Subscript[a, j]))L, ξ->(∂_(Subscript[x, i]))Q}]]

c𝕠=C𝕆[𝔼[ℏ (Subscript[t, 1])(Subscript[a, 2]),ℏ (Subscript[t, 1]^(-1))((E^(Subscript[t, 1]))-1)(Subscript[y, 1])(Subscript[x, 2]),1+ϵ (Subscript[x, 1])(Subscript[y, 2])], (Subscript[{(Subscript[y, 1]),(Subscript[x, 1])}, 1]), (Subscript[{(Subscript[x, 2]),(Subscript[a, 2]),(Subscript[y, 2])}, 2])]

(Subscript[SW, (Subscript[x, 2]),(Subscript[a, 2])])[c𝕠 ]

With[{c𝕠=C𝕆[(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]),1+ϵ (Subscript[x, 1])(Subscript[y, 2])]]},
HL[CU[c𝕠]==CU[c𝕠//(Subscript[SW, (Subscript[x, 2]),(Subscript[a, 2])])]]]

With[{c𝕠=C𝕆[(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])),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]))]]},
{CU[c𝕠]//Short,HL[CU[c𝕠]==CU[c𝕠//(Subscript[SW, (Subscript[x, 2]),(Subscript[a, 2])])]]}
]

(Subscript[SW, (Subscript[x, i_]),(Subscript[y, j_])->k_])[C𝕆[(Subscript[{lh___,(Subscript[x, i_]),(Subscript[y, j_]),rh___}, s_]),more___,𝔼[L_,Q_,P_]]] := C𝕆[(Subscript[{lh,(Subscript[y, k]),(Subscript[a, k]),(Subscript[x, k]),rh}, s]),more,
With[{q=ν(ξ (Subscript[x, k])+η (Subscript[y, k])+δ (Subscript[x, k]) (Subscript[y, k])-(Subscript[t, k]) ξ η)},
𝔼[L,q+(Q/.(Subscript[x, i])|(Subscript[y, j])->0), (E^(-q))(Subscript[DP, (Subscript[x, i])->(Subscript[D, ξ]),(Subscript[y, j])->(Subscript[D, η])])[P][CΛ[(Subscript[t, k]),(Subscript[y, k]),(Subscript[a, k]),(Subscript[x, k]),ξ,η,δ](E^q)]] /. ν->(((1+(Subscript[t, k])δ))^(-1))/. {ξ->((∂_(Subscript[x, i]))Q/.(Subscript[y, j])->0), η->((∂_(Subscript[y, j]))Q/.(Subscript[x, i])->0), δ->(∂_((Subscript[x, i]),(Subscript[y, j])))Q}]]

With[{c𝕠=C𝕆[(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])),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]))]]},
{CU[c𝕠]//Short,HL[CU[c𝕠]==CU[c𝕠//(Subscript[SW, (Subscript[x, 1]),(Subscript[y, 1])->1])]]}
]

The Quantum Logos QΛ

Goal 1: In QU, compute F=(e^(-ηy))(e^(ξx))(e^(ηy))(e^(-ξx)).

First compute G=(e^(ξx))((ye)^(-ξx)), a finite sum.

adx[ℰ_]:=Simp[QU@x ** ℰ - ℰ ** QU@x];
G=Simp[NestList[adx, QU@y, $TϵD+1].Table[(ξ^k)/k!, {k,0, $TϵD+1}]]

G/.ϵ->0

Now F satisfies the ODE (∂_η)F=(∂_η)((e^(-ηy))(e^(ηG)))=-yF+FG with initial conditions F(η=0)=1. We set it up and solve:

F=Sum[(Subscript[f, l,i,j,k])[η](ϵ^l)QU@{(y^i),(a^j),(x^k)},{l,0,$TϵD},{i,0, l},{j,0, l},{k,0, Min[l,2l-i-j]}]

unowns=Cases[F, (Subscript[f, ___])[η],∞]

bas=Union@@Table[(ϵ^l)Cases[Coefficient[F,ϵ,l],_QU,∞], {l,0,$TϵD}]

Short[eqns=Flatten[{(Coefficient[F-QU[], #]/.η->0)==0, Expand[Coefficient[Simp[F**G-QU[y]**F-(∂_η)F], #]]==0}& /@ bas], 8]

Short[{sol}=DSolve[eqns, unowns, η], 8]

Union@Cases[sol,(E^(_)),∞]

FF=Collect[F/.sol/.{(E^(_))->1, QU->Times}, ϵ, Simplify]

{Short[lhs=SimpT@(Subscript[𝕆, QU])[SS[(E^(ℏ(ξ x+η y)))],{x,y}], 5], HL[lhs==SimpT@(Subscript[𝕆, QU])[SS[(E^(ℏ(ξ x+η y+(1-(T^2))ξ η)))(FF/.{ξ->ℏ ξ, η->ℏ η})],{y,a,x}]]}

QΛ[T_,y1_,a1_,x1_,ξ1_,η1_,δ_]:=Module[
{adx,G,F,f,unowns,bas,eqns,sol,λ,q,ν, ξ, η,t},
adx[ℰ_]:=Simp[(Subscript[x, QU]) ** ℰ - ℰ ** (Subscript[x, QU])];
G=Simp[NestList[adx, (Subscript[y, QU]), $TϵD+1].Table[(ξ^k)/k!, {k,0, $TϵD+1}]];
F=Sum[(Subscript[f, l,i,j,k])[η](ϵ^l)QU@{(y^i),(a^j),(x^k)},{l,0,$TϵD},{i,0, l},{j,0, l},{k,0, Min[l,2l-i-j]}];
unowns=Cases[F, (Subscript[f, ___])[η],∞];
bas=Union@@Table[(ϵ^l)Cases[Coefficient[F,ϵ,l],_QU,∞], {l,0,$TϵD}];
eqns=Flatten[{(Coefficient[F-QU[], #]/.η->0)==0, Expand[Coefficient[Simp[F**G-(Subscript[y, QU])**F-(∂_η)F], #]]==0}& /@ bas];
{sol}=DSolve[eqns, unowns, η];
λ=Collect[F/.sol/.{(E^(_))->1, QU->Times}, ϵ, Simplify];
q=(E^(ν(-t ξ η+η y+ξ x+δ y x)));
Collect[ν (q^(-1))(Subscript[DP, ξ->(Subscript[D, x]),η->(Subscript[D, y])])[λ][q] /. ν->(((1+t δ))^(-1))/.t->((T^2)-1)/ℏ,ϵ,Simplify] /. {y->y1,a->a1,x->x1,ξ->ξ1, η->η1}
];

QΛ[T,y,a,x,ξ,η,δ]

{Short[lhs=SimpT@(Subscript[𝕆, QU])[SS[(E^(ℏ(ξ x+η y+δ x y)))],{x,y}], 5],

rhs=SimpT@(Subscript[𝕆, QU])[SS[(E^(ℏ ν(ξ x+η y+δ x y-((T^2)-1) ξ η)))QΛ[T,y,a,x,ℏ ξ,ℏ η,ℏ δ] /. ν ->(((1+((T^2)-1) δ))^(-1))],{y,a,x}];
HL[Simplify[lhs==rhs]]}

Stitching Direct

MatrixExp[(Subscript[η, 1])ρ[CU@y]].MatrixExp[(Subscript[α, 1])ρ[CU@a]].MatrixExp[(Subscript[ξ, 1])ρ[CU@x]].MatrixExp[(Subscript[η, 2])ρ[CU@y]].MatrixExp[(Subscript[α, 2])ρ[CU@a]].MatrixExp[(Subscript[ξ, 2])ρ[CU@x]] // Simplify // MatrixForm

eqn=MatrixExp[(Subscript[η, 1])ρ[CU@y]].MatrixExp[(Subscript[α, 1])ρ[CU@a]].MatrixExp[(Subscript[ξ, 1])ρ[CU@x]].MatrixExp[(Subscript[η, 2])ρ[CU@y]].MatrixExp[(Subscript[α, 2])ρ[CU@a]].MatrixExp[(Subscript[ξ, 2])ρ[CU@x]] == (E^(τ0 ϵ γ))MatrixExp[η0 ρ[CU@y]].MatrixExp[α0 ρ[CU@a]].MatrixExp[ξ0 ρ[CU@x]]

sol=Block[{ϵ},Solve[Thread[Flatten/@eqn], {τ0,η0,α0,ξ0}]][[1]]

eqn=MatrixExp[(Subscript[η, 1])ρ[CU@y]].MatrixExp[(Subscript[α, 1])ρ[CU@a]].MatrixExp[(Subscript[ξ, 1])ρ[CU@x]].MatrixExp[(Subscript[η, 2])ρ[CU@y]].MatrixExp[(Subscript[α, 2])ρ[CU@a]].MatrixExp[(Subscript[ξ, 2])ρ[CU@x]] == T0 MatrixExp[η0 ρ[CU@y]].MatrixExp[α0 ρ[CU@a]].MatrixExp[ξ0 ρ[CU@x]]

sol=Block[{ϵ},Solve[Thread[Flatten/@eqn], {T0,η0,α0,ξ0}]][[1]]

𝔼

𝔼[L,Q,P] means (e^(ℏ(L+Q)))P, where L is linear in the a’s, Q is a combination of (Subscript[x, i])(Subscript[y, j]), and P is a perturbation polynomial. It should be interpreted via C𝕆[𝔼[...], (Subscript[{(Subscript[x, 1]), (Subscript[a, 1]), (Subscript[y, 1])}, i]),...] (with some default for direct interpretation), or likewise via Q𝕆[𝔼[...], (Subscript[{(Subscript[x, 1]), (Subscript[a, 1]), (Subscript[y, 1])}, i]),...]. In themselves, C𝕆 and Q𝕆 should have an interpretation in CU/QU by casting.