(* ############################################################### *)
(* ###  Ancillary computations for:                                #### *)
(* ### "Flux Quantization on 11d Superspace"                       #### *)
(* ## (HyperlinkTemplate[ncatlab.org/schreiber/show/Flux+Quantization+on+11d+Superspace, https://ncatlab.org/schreiber/show/Flux+Quantization+on+11d+Superspace, https://ncatlab.org/schreiber/show/Flux+Quantization+on+11d+Superspace, HyperlinkActionRecycled, HyperlinkActive, , ]) ## *)
(* ############################################################### *)

(* Here: Verification that, assuming flux- and torsion-Bianchis, the gravitino Bianchi is equivalent to the Rarita-Schwinger equation, 
which in turn implies the Einstein equation. *)

(* With attention to the converse direction that has been rarely or never 
been discussed in the literature: Namely proof that with the flux- and torsion-
Bianchis and the -component of the gravitino Bianchi satisfied, the 
remaining - and -components of the gravitino Bianchi follow. 
The check of the -component takes two orders of magnitude more computing
time than all other checks combined. *)

(*--- 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

Remark.  The command (HyperlinkTemplate[GammaExtract, https://arxiv.org/pdf/hep-th/0105086.pdf#page=6, https://arxiv.org/pdf/hep-th/0105086.pdf#page=6, HyperlinkActionRecycled, HyperlinkActive, , ]) provided by Gamma.m simplifies tensor-spinor expressions of the form  by assuming the irreducibility condition .
In the following,first the -component of the gravitino Bianchi is seen to imply this condition for the component  of the gravitino field strength; which is then used, via GammaExtract, to show that this same -component implies no further condition on  beyond its Rarita-Schwinger equation of motion.
Afterwards,the irreducibility condition satisfied by the irreps  is used, via GammaExtract, to show that the - and -component of the gravitino Bianchi identity is identically satisfied.
(All this assuming that the flux- and the torsion Bianchi identities have already been solved.)

(*-- equation (131), for later use --*)
H[a_]:=(
(1/6)*(1/3!)*Tensor[G4,{a,z1,z2,z3}]**GammaProd[{z1,z2,z3}]
-(1/12)*(1/4!)*Tensor[G4,{z1,z2,z3,z4}]**GammaProd[{a,z1,z2,z3,z4}]
)

(*--- Checks for Lemma 3.2 ---*)

(*-- equation (141) --*)

Simplify[
-(2/6)*(1/5!)*(1/3!)*3!*Binomial[5,3]*Binomial[3,3]
+ (2/12)*(1/5!)*(1/4!)*4!*Binomial[5, 4]*Binomial[4,4]
+(1/2)*(1/4!) 
]

Simplify[
-(2/6)*(1/5!)*(1/3!) *1* Binomial[5,1]*Binomial[3,1]
+(2/12)*(1/5!)*(1/4!)*2*Binomial[5,2]*Binomial[4,2]
 ]

(*--- Checks for Lemma 3.5---*)

(*-- checking   in equation (144) --*)
Simplify[
GammaExtract[
GammaContract[GammaExpand[
GammaProd[
{a1,a2,a3,a4,a5,a6,a7, b1,b2,b3,b4},
{b1,b2}
]**TensorSpinor[rho,{b3,b4}]
-84*
ASym[
GammaProd[{a1,a2,a3,a4,a5}]**TensorSpinor[rho,{a6,a7}],
{a1,a2,a3,a4,a5,a6,a7}
]
]]
]
]

(*------------  Checks for Lemma 3.6  ---------------*)

(*--- (151)-- checking  ---*)
Simplify[
RenameDummy[
GammaExtract[
GammaContract[GammaExpand[
GammaProd[{a1,a2,a3,a4}]**
ASym[
  GammaProd[{a1,a2}]**
Tensor[D, {a3}]
**TensorSpinor[rho,{a4,a5}],
{a1,a2,a3,a4,a5}
]
]]
]
]
]
-(84/5) (Subscript[D, d0]) (Subscript[(OverTilde[rho]), a5d0])

(*--- (152) -- checking  ---*)
Simplify[
RenameDummy[
GammaExtract[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
GammaProd[{b1,b2}]**
ASym[
  GammaProd[{b1,b2}]**
Tensor[D, {a1}]*TensorSpinor[rho,{a2,a3}],
{b1,b2,a1,a2,a3}
]
+3*
ASym[
Tensor[D,{a1}]* TensorSpinor[rho,{a2,a3}],
{a1,a2,a3}
]
+ (1/5)*ASym[
GammaProd[{a1,a2}]**
Tensor[D,{b}]*TensorSpinor[rho,{b,a3}],
{a1,a2,a3}
]
-ASym[
GammaProd[{b,a1}]**
Tensor[D,{b}]*TensorSpinor[rho,{a2,a3}],
{a1,a2,a3}
]
]]
]]
]
]
]
0

(*------------  Checks for Lemma 3.7   --------------*)

(*+++ The -component of the gravitino Bianchi +++++*)

(* --------- The coefficient of  ------------ *)
Simplify[ 
RenameDummy[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
(*  *)
32 * TensorSpinor[rho,{c,a}]
+ 
(**)
(-1/3)*
  GammaProd[
{b1,b2,b3},
{c}
]
**
ASym[
GammaProd[{a,b1}]
**TensorSpinor[rho,{b2,b3}],
{a, b1,b2,b3}
]
+
(**)
(+1/24)*
GammaProd[
{a,b1,b2,b3,b4},
{c},
{b1,b2}]**TensorSpinor[rho,{b3,b4}]
+
(**)
(-1/4) *
GammaProd[
{b1,b2},
{c},
{b1}]**TensorSpinor[rho,{b2,a}]
+
 (+1/4) *
GammaProd[
{b1,b2},
{c},
{a}]**TensorSpinor[rho,{b1,b2}]
+
(-1/4) *
GammaProd[
{b1,b2},
{c},
{b2}]**TensorSpinor[rho,{a,b1}]

]]]]
]]]]

(*--- (163) -- its contractions imply the gravitino equation and irreducibility: ---*)
Simplify[
RenameDummy[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
GammaProd[{c}]** %
]]
]]]
]
Simplify[
RenameDummy[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
GammaProd[{a}]** %%
]]
]]]
]

(*-- (165) -- conversely, irreducibility implies this component of the Bianchi: ---*)
GammaExtract[
  %%%
]

(*------- The coefficient of   -------*)
Simplify[ 
RenameDummy[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
GammaContract[GammaExpand[ 
(*    *)
(-1/3)*
  GammaProd[
{b1,b2,b3},
{c1, c2}
]
**
ASym[
GammaProd[{a,b1}]
**TensorSpinor[rho,{b2,b3}],
{a, b1,b2,b3}
]
+
(*    *)
(+1/24)*
GammaProd[
{a,b1,b2,b3,b4},
{c1, c2},
{b1,b2}]**TensorSpinor[rho,{b3,b4}]
+
(*    *)
(-1/4) *
GammaProd[
{b1,b2},
{c1, c2},
{b1}]**TensorSpinor[rho,{b2,a}]
+
 (+1/4) *
GammaProd[
{b1,b2},
{c1, c2},
{a}]**TensorSpinor[rho,{b1,b2}]
+
(-1/4) *
GammaProd[
{b1,b2},
{c1, c2},
{b2}]**TensorSpinor[rho,{a,b1}]

]]]]
]]]]

(*-- (165) -- irreducibility implies this component of the Bianchi:  ---*) 
GammaExtract[%]

(*---  The coefficient of   ---*)
Simplify[ 
RenameDummy[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
GammaContract[GammaExpand[ 
(*    *)
(-1/3)*
  GammaProd[
{b1,b2,b3},
{c1, c2, c3, c4, c5}
]
**
ASym[
GammaProd[{a,b1}]
**TensorSpinor[rho,{b2,b3}],
{a, b1,b2,b3}
]
+
(*    *)
(+1/24)*
GammaProd[
{a,b1,b2,b3,b4},
{c1, c2, c3, c4, c5},
{b1,b2}]**TensorSpinor[rho,{b3,b4}]
+
(*    *)
(-1/4) *
GammaProd[
{b1,b2},
{c1, c2, c3, c4, c5},
{b1}]**TensorSpinor[rho,{b2,a}]
+
 (+1/4) *
GammaProd[
{b1,b2},
{c1, c2, c3, c4, c5},
{a}]**TensorSpinor[rho,{b1,b2}]
+
(-1/4) *
GammaProd[
{b1,b2},
{c1, c2,c3, c4, c5},
{b2}]**TensorSpinor[rho,{a,b1}]

]]]]
]]]]

(*-- nudge Mathematica to discard the terms proportional to   ---*)
ASym[%,{c1,c2,c3,c4,c5}]

(*-- (165) --- irreducibility implies this component of the Bianchi ---*)
GammaExtract[%]

(*+++ Checking the -component of the Gravitino Bianchi +++*)
(*-- p. 49 --*)

(*--- the term proportional to   ---*)
GammaContract[GammaExpand[
(-1/6)*(1/3!)* (1/11) *
ASym[
GammaProd[
{a1,a2, a3},
{a4}
],
{a1,a2,a3,a4}
]
**
TensorSpinor[Xi,{}]
+
(-1/12)*(1/4!)* (1/11)*
GammaProd[
{b, a1, a2, a3, a4},
{b}
]
**
TensorSpinor[Xi,{}]
+
(1/(4*6))* (1/11)
ASym[
GammaProd[
{a1, a2}, 
{a3,a4}
],
{a1,a2,a3,a4}
]
**
TensorSpinor[Xi,{}]
+
(1/(4*6))*(1/24)*(-1/77)*(1/5!)*
GammaProd[
{b1,b2},
{b1,b2, a1, a2, a3, a4, c1, c2, c3, c4, c5}, (*the LC symbol*)
{c1, c2, c3, c4, c5}
]
**
TensorSpinor[Xi,{}]
]]

(*-- make the system recall the skew-symmetry --*)
ASym[
 %,
{a1,a2,a3,a4}
]

(*--- the term proportional to   ---*)

GammaExtract[
GammaContract[GammaExpand[
(-1/6)*(1/3!)*
ASym[
GammaProd[
{a1,a2, a3}
]
**
TensorSpinor[Xi,{a4}]
,
{a1,a2,a3,a4}
]
+
(-1/12)*(1/4!)*
GammaProd[
{b, a1, a2, a3, a4}
]
**
TensorSpinor[Xi,{b}]
+
(1/(4*6))* (-2/9)*
ASym[
GammaProd[
{a1, a2}
]
**
ASym[
GammaProd[{a3}] **
TensorSpinor[Xi,{a4}],
{a3, a4}
],
{a1,a2,a3,a4}
]
+
(1/(4*6))*(1/24)*(5/9)*(1/5!)*
GammaProd[
{b1,b2},
{b1,b2, a1, a2, a3, a4, c1, c2, c3, c4, c5} (*LC symbol*) 
]
**
ASym[
GammaProd[{c1, c2, c3, c4}]
**
TensorSpinor[Xi,{c5}],
{c1, c2, c3, c4, c5}
]
]]
]

(*--- the term proportional to   ---*)

GammaExtract[GammaExpand[
GammaExtract[GammaExpand[
(1/(4*6))*
ASym[
GammaProd[
{a1, a2}
]
**
TensorSpinor[Xi,{a3,a4}],
{a1,a2,a3,a4}
]
+
(1/(4*6))*(1/24)*2*(1/5!)*
GammaProd[
{b1,b2},
{b1,b2, a1, a2, a3, a4, c1, c2, c3, c4, c5}, (*the LC symbol*)
{c1, c2, c3}
]
**
TensorSpinor[Xi,{c4, c5}]
]]
]]

(*--- the term proportional to   ---*)

GammaExtract[GammaExpand[
(1/(4*6))*(1/24)*(1/5!)
GammaProd[
{b1,b2},
{b1,b2, a1, a2, a3, a4, c1, c2, c3, c4, c5} (*the LC symbol*)
]
**
TensorSpinor[Xi,{c1, c2, c3, c4, c5}]
]]

(*--- Checking the -component of the Gravitino Bianchi ---*)

(*-- first to state the covariant derivative of  in stages --*)
(*-- using Lemma 3.6 --*)

(*-- (132)  --*)
H[a_]:=(
(1/6)*(1/3!)*Tensor[G4,{a,z1,z2,z3}]**GammaProd[{z1,z2,z3}]
-(1/12)*(1/4!)*Tensor[G4,{z1,z2,z3,z4}]**GammaProd[{a,z1,z2,z3,z4}]
)

(*-- (153) --*)
barH[a_]:=(
(1/6)*(1/3!)*Tensor[G4,{a,z1,z2,z3}]**GammaProd[{z1,z2,z3}]
+(1/12)*(1/4!)*Tensor[G4,{z1,z2,z3,z4}]**GammaProd[{a,z1,z2,z3,z4}]
)

(*-- (148) --*)
FiveIndexDerivative[a1_,a2_,a3_,a4_,a5_]:=(
Simplify[
GammaExtract[
GammaContract[GammaExpand[
ASym[
barH[a1]**GammaProd[{a2,a3}]**TensorSpinor[rho,{a4,a5}],
{a1,a2,a3,a4,a5}
]
- 
(1/3)*
ASym[
Tensor[G4,{y,a1,a2,a3}]*GammaProd[{y}]**TensorSpinor[rho,{a4,a5}],
{a1,a2,a3,a4,a5}
]
]]
]
]
)

(*-- (149) --*)
DivergenceOfRho[a_]:=(
Simplify[
GammaExtract[
GammaContract[GammaExpand[
(5/84)*
GammaProd[{x1,x2,x3,x4}]**
FiveIndexDerivative[x1,x2,x3,x4,a]
]]
]
]
)

(*-- (150) --*)
ThreeIndexDerivative[c1_,c2_,c3_]:=(
Simplify[GammaExtract[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
-ASym[
GammaProd[{c1,c2}]**DivergenceOfRho[c3],
{c1,c2,c3}
]
+2*
barH [w]**
ASym[
GammaProd[{w,c1}]**TensorSpinor[rho,{c2,c3}],
{w,c1,c2,c3}
]
+(2*5! *84/(7! *4!))*
GammaProd[{c1,c2,c3,w1,w2,w3,w4,w5,w6,w7,w8}]**(
(12/(4!*4!))*
Tensor[G4,{w1,w2,w3,w4}]*GammaProd[{w5,w6}]**TensorSpinor[rho,{w7,w8}]
-
(1/6!)* (1/4!)*Tensor[G4,{v1,v2,v3,v4}]*GammaProd[{u,w1,w2,w3,w4,w5,w6,v1,v2,v3,v4}]
**GammaProd[{u}]**TensorSpinor[rho,{w7,w8}]
)
]]
]]
]]
)

(*-- (147) --*)
ExteriorDerivativeOfRho[a1_,a2_,a3_] :=(
(1/3)*
ThreeIndexDerivative[a1,a2,a3]
-(1/15)*
ASym[
GammaProd[{a1, a2}]**DivergenceOfRho[a3],
{a1,a2,a3}
]
-(1/3)*
GammaProd[{s1,s2}]**FiveIndexDerivative[s1,s2,a1,a2,a3]
)

(*--- now with these definitions, the actual check mentioned on p. 49 --*)

Simplify[RenameDummy[
GammaExtract[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
(*-- The -component of the gravitino Bianchi --*)
ExteriorDerivativeOfRho[a1,a2,a3]
+ 
ASym[
H[a1]**TensorSpinor[rho,{a2,a3}],
{a1,a2,a3}
]
(*----*)
]]
]]
]
]]

(*--- Checks for Lemma 3.8---*)
(*--- Deriving the Einstein equation from the gravitino equation---*)

(*-- expanding the -term (B) --*)
Simplify[
RenameDummy[
GammaContract[GammaExpand[
GammaContract[GammaExpand[
GammaProd[{a,b1,b2}]**
(
(1/6)*(1/3!)*
Tensor[G4,{b1,c1,c2,c3}]**
GammaProd[{c1,c2,c3}]
-
(1/12)*(1/4!)*
Tensor[G4,{c1,c2,c3,c4}]**
GammaProd[{b1,c1,c2,c3,c4}]
)**
(
(1/6)*(1/3!)*
Tensor[G4,{b2,d1,d2,d3}]**
GammaProd[{d1,d2,d3}]
-
(1/12)*(1/4!)*
Tensor[G4,{d1,d2,d3,d4}]**
GammaProd[{b2,d1,d2,d3,d4}]
)
]]
]]
]
-
(-1/24)(
GammaProd[{d0}]*Tensor[G4,{a,d1,d2,d3}]*Tensor[G4,{d0,d1,d2,d3}]
-
(1/8)GammaProd[{a}]*Tensor[G4,{d0,d1,d2,d3}]^2 
)
]

(*-- no 1-index Gamma-term left: --*)

% /. {
GammaProd[{a1_,a2_,a3_}] -> 0,
GammaProd[{a1_, a2_,a3_,a4_,a5_,a6_,a7_}]->0,
GammaProd[{a1_, a2_,a3_,a4_,a5_,a6_,a7_, a8_,a9_}]->0
}