Pensieve header: Verifying the full set of KV equations in Γ-calculus.

KV solutions probably coming from pensieve://2012-05/beta5.1/betaExact.nb.

SetDirectory["C:/drorbn/AcademicPensieve/Projects/MetaCalculi/"];
<< "MetaCalculi.m"

ΓSimp=Assuming[(Subscript[T, 1])>1∧(Subscript[T, 2])>1∧(Subscript[T, 3])>1, Simplify[PowerExpand[#]]]&;
R[i_,j_] := Γ[Xp[i,j]];

{V0=Γ[V], V0i=Γ[Vi], V0**V0i} // ColumnForm

MatrixForm@Simplify[(({{(((((((-1+(Subscript[T, 1]))/(Log[(Subscript[T, 1])]))))^(1/4)) (((((-1+(Subscript[T, 2]))/(Log[(Subscript[T, 2])]))))^(1/4)))/(((((-1+(Subscript[T, 1]) (Subscript[T, 2]))/(Log[(Subscript[T, 1]) (Subscript[T, 2])]))))^(1/4))), (Subscript[s, 1]), (Subscript[s, 2])}, {(Subscript[s, 1]), ((Log[(Subscript[T, 1])]+(Sqrt[((Log[(Subscript[T, 1])] Log[(Subscript[T, 2])] Log[(Subscript[T, 1]) (Subscript[T, 2])] (Subscript[T, 1]) (-1+(Subscript[T, 2])))/((-1+(Subscript[T, 1])) (-1+(Subscript[T, 1]) (Subscript[T, 2]))))]))/(Log[(Subscript[T, 1]) (Subscript[T, 2])])), ((Log[(Subscript[T, 1])]-(Subscript[T, 2]) (Sqrt[((Log[(Subscript[T, 1])] Log[(Subscript[T, 2])] Log[(Subscript[T, 1]) (Subscript[T, 2])] (-1+(Subscript[T, 1])) (Subscript[T, 1]))/((-1+(Subscript[T, 2])) (-1+(Subscript[T, 1]) (Subscript[T, 2]))))]))/(Log[(Subscript[T, 1]) (Subscript[T, 2])]))}, {(Subscript[s, 2]), ((Log[(Subscript[T, 2])]-(Sqrt[((Log[(Subscript[T, 1])] Log[(Subscript[T, 2])] Log[(Subscript[T, 1]) (Subscript[T, 2])] (Subscript[T, 1]) (-1+(Subscript[T, 2])))/((-1+(Subscript[T, 1])) (-1+(Subscript[T, 1]) (Subscript[T, 2]))))]))/(Log[(Subscript[T, 1]) (Subscript[T, 2])])), ((Log[(Subscript[T, 2])]+(Subscript[T, 2]) (Sqrt[((Log[(Subscript[T, 1])] Log[(Subscript[T, 2])] Log[(Subscript[T, 1]) (Subscript[T, 2])] (-1+(Subscript[T, 1])) (Subscript[T, 1]))/((-1+(Subscript[T, 2])) (-1+(Subscript[T, 1]) (Subscript[T, 2]))))]))/(Log[(Subscript[T, 1]) (Subscript[T, 2])]))}, {"Γ", 1, (Sqrt[(Subscript[T, 1])])}}))/. Log[x_]:>PowerExpand@Log[x/.(Subscript[T, i_]^(p_.))->(E^(p (Subscript[t, i])))]]

(({{((((((((Subscript[T, 1])-1)/(Subscript[t, 1]))))^(1/4)) ((((((Subscript[T, 2])-1)/(Subscript[t, 2]))))^(1/4)))/((((((Subscript[T, 1]) (Subscript[T, 2])-1)/((Subscript[t, 1])+(Subscript[t, 2])))))^(1/4))), (Subscript[s, 1]), (Subscript[s, 2])}, {(Subscript[s, 1]), (((Subscript[t, 1])+(Sqrt[(((Subscript[t, 1]) (Subscript[t, 2]) ((Subscript[t, 1])+(Subscript[t, 2])) (Subscript[T, 1]) ((Subscript[T, 2])-1))/(((Subscript[T, 1])-1) ((Subscript[T, 1]) (Subscript[T, 2])-1)))]))/((Subscript[t, 1])+(Subscript[t, 2]))), (((Subscript[t, 1])-(Subscript[T, 2]) (Sqrt[(((Subscript[t, 1]) (Subscript[t, 2]) ((Subscript[t, 1])+(Subscript[t, 2])) ((Subscript[T, 1])-1) (Subscript[T, 1]))/(((Subscript[T, 2])-1) ((Subscript[T, 1]) (Subscript[T, 2])-1)))]))/((Subscript[t, 1])+(Subscript[t, 2])))}, {(Subscript[s, 2]), (((Subscript[t, 2])-(Sqrt[(((Subscript[t, 1]) (Subscript[t, 2]) ((Subscript[t, 1])+(Subscript[t, 2])) (Subscript[T, 1]) ((Subscript[T, 2])-1))/(((Subscript[T, 1])-1) ((Subscript[T, 1]) (Subscript[T, 2])-1)))]))/((Subscript[t, 1])+(Subscript[t, 2]))), (((Subscript[t, 2])+(Subscript[T, 2]) (Sqrt[(((Subscript[t, 1]) (Subscript[t, 2]) ((Subscript[t, 1])+(Subscript[t, 2])) ((Subscript[T, 1])-1) (Subscript[T, 1]))/(((Subscript[T, 2])-1) ((Subscript[T, 1]) (Subscript[T, 2])-1)))]))/((Subscript[t, 1])+(Subscript[t, 2])))}, {Γ, 1, (Sqrt[(Subscript[T, 1])])}}))

Testing dΔ

{γ0=Γ[ω, (Subscript[h, a])(Subscript[σ, a])+(Subscript[h, z])(Subscript[σ, z]), {(Subscript[t, a]),(Subscript[t, z])}.(({{α, θ}, {ϕ, Ξ}})).{(Subscript[h, a]),(Subscript[h, z])}],
t1=γ0 // A // dΔ[a,x,y] // Γ,
t2=γ0 // dΔ[a,x,y],
t1==t2 // Simplify}

The Hard R4 Equation

(R[2,3]**R[1,3]**V0)==(V0**(R[1,3] // dΔ[1,1,2])) // ΓSimp

The Twist Equation

Θ[1,2] // Γ

V0**(Θ[1,2] // Γ) == R[1,2]**(V0 // dσ[1->2, 2->1]) // ΓSimp

The Unitarity Equation

(V0**(V0 // dA[1,2]) == (ϵ[1]ϵ[2] // Γ)) // ΓSimp

The Vertical Flip Equation

(V0**(V0 // dS[1,2]) == R[1,2]) // ΓSimp

The Cap Equation

Not tested now / not quite meaningful in Γ.