(* ############################################################ *)
(* ### Ancillary computation for:                                ### *)
(* ### "Flux Quantization on M5-Branes"                          ### *)
(* ### ncatlab.org/schreiber/show/Flux+Quantization+on+M5-Branes ### *)
(* ############################################################ *)

(* Verification of a couple of the more tedious Clifford contractions *)

(*--- load package for Clifford algebra ---*)
(*--- (HyperlinkTemplate[fy.chalmers.se/~ulfgran/gamma.htm, https://fy.chalmers.se/~ulfgran/gamma.htm, https://fy.chalmers.se/~ulfgran/gamma.htm, HyperlinkActionRecycled, HyperlinkActive, , ]) ---*)
<< Gamma.m

SetDim[6]

Dim

(* Proof of Lemma 3.10 *)

Simplify[
Simplify[RenameDummy[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
(
(1/3!)*Tensor[H3,{b1,b2,b3}]*GammaProd[{b1,b2,b3}]
)
**GammaProd[{a}]**
(
(1/3!)*Tensor[H3,{c1,c2,c3}]*GammaProd[{c1,c2,c3}]
)
]]
]]
/.{
  Tensor[H3,{a_,c4_,c5_}]
*GammaProd[{c1_,c2_,c3_,c4_,c5_}]
->
(4!*2)/(3!)
*Tensor[H3,{x1,x2,x3}]
*Delta[
  {c1,c2,c3,ap},
  {x1,x2,x3, a }
]
GammaProd[{ap}]
}
]]
/.{
Tensor[H3,{a_,b_,c_}]*Tensor[H3,{a_,b_,c_}]
->
0
,
GammaProd[{a_,b1_,b2_}]
*
Tensor[H3,{b1_,c1_,c2_}]*Tensor[H3,{b2_,c1_,c2_}]
->
0
}
]