AI on geometric computation and verification
Further Updates
(Mar 23) Use hybrid formalization to verify Proposition 3.6.
Introduction
\(4\)-dimensional double null equations of Lorentzian manifold is well-known for General Relaticity mathmaticians, but the computation is so complex that most of the mathematicians are using the schematical format because they don’t have enough energy and accuracy to do all of the computation and verify the equations.
This time, I want to test if ChatGPT 5.4 Pro can handle all of the derivation and verification. So I asked it to derive the higher dimensional null equations based on notations in this article. The equations are schematical in the article but I required GPT to output the entire equations with complete derivation process. After finishing the equations derivation, which took around 2.5 hours, I required Codex to verify all the equations. The results were shocking. Because the equations are symmetric, one equation has a twin. There were typos in few equations, but the twin equations were coprrect so the mistakes were completely ignorable. Except these, GPT finished all computation correctly.
Below is the problem setting and some of the equations, so readers can have the concept of the difficulty.
Settings and equations
Let \((\mathcal M^{n+2},g)\) be Lorentzian and suppose that, in double-null coordinates \((u,v,\theta^1,\dots,\theta^n)\), \[\begin{equation} g = -2\Omega^2( d u\otimes d v+ d v\otimes d u) +\gamma_{AB}( d\theta^A-b^A d u)( d\theta^B-b^B d u). \end{equation}\] The null frame adapted to this gauge is \[\begin{equation} e_4=\Omega^{-1}\partial_v, \qquad e_3=\Omega^{-1}\bigl(\partial_u+b^A\partial_A\bigr), \qquad e_A\in TS_{u,v}, \end{equation}\] with \[\begin{equation} g(e_3,e_4)=-2, \qquad g(e_A,e_B)=\gamma_{AB}, \qquad g(e_A,e_3)=g(e_A,e_4)=0. \end{equation}\] All tangential indices are raised and lowered with \(\gamma\); all angular covariant derivatives are those of \((S_{u,v},\gamma)\) and are denoted simply by \(\nabla_A\).
We use the conventions \[ \begin{aligned} \chi_{AB}&=g(D_A e_4,e_B),& \underline\chi_{AB}&=g(D_A e_3,e_B),\\ \eta_A&=-\frac12 g(D_3 e_A,e_4),& \underline\eta_A&=-\frac12 g(D_4 e_A,e_3),\\ \omega&=-\frac14 g(D_4 e_3,e_4),& \underline\omega&=-\frac14 g(D_3 e_4,e_3),\\ \zeta_A&=\frac14 g([e_3,e_4],e_A). \end{aligned} \]
We write \[ \begin{align} \alpha_{AB}&=R_{A4B4},& \underline\alpha_{AB}&=R_{A3B3},\\ \beta_A&=\frac12 R_{A434},& \underline\beta_A&=\frac12 R_{A334},\\ \rho&=\frac14 R_{3434},& \sigma_{AB}&=\frac12 R_{34AB},\\ \tau_{AB}&=\frac12(R_{3A4B}+R_{3B4A}),& \nu_{ABC}&=R_{AB C4},\qquad \underline\nu_{ABC}=R_{AB C3}. \end{align} \] Thus \(\tau_{AB}\) is symmetric, \(\sigma_{AB}\) is antisymmetric, and \(\nu,\underline\nu\) are antisymmetric in their first two indices.
For a symmetric tangential \(2\)-tensor \(k\) we write \[\begin{equation} k=\hat k+\frac1n( {\text{tr}} k)\,\gamma. \end{equation}\] The symmetric tracefree part of a tangential tensor \(X_{AB}\) is denoted by \(\widehat{X}_{AB}\).
Below is part of the equations.
\[ \begin{align} \nabla_3\alpha_{AB} ={}&4\underline\omega\,\alpha_{AB} -2\underline\eta^C\nu_{C(AB)} -2\underline\eta_{(A}\beta_{B)} -\nabla_4\tau_{AB} \notag\\ &\quad +2{\text{Sym}}_{AB}\Bigl[ -\nabla^C\nu_{CAB}-\zeta^C\nu_{CAB} -\tfrac12{\text{tr}}\chi\,(\tau_{AB}+\sigma_{AB}) -\tfrac12{\text{tr}}\underline\chi\,\alpha_{AB} \notag\\ &\qquad\qquad +\tfrac12\chi_A{}^C(\tau_{CB}+\sigma_{CB}) +\tfrac12\underline\chi_A{}^C\alpha_{CB} -\chi^{CD}R_{CADB} +\chi_B{}^C\sigma_{CA} \Bigr], \label{eq:b1}\\[0.8ex] \nabla_4\beta_A ={}& \nabla^B\alpha_{BA} +(2\zeta^B+\eta^B)\alpha_{BA} -\hat\chi_A{}^B\beta_B -\hat\chi^{BC}\nu_{ABC} \notag\\ &\quad -\Bigl(1+\frac2n\Bigr){\text{tr}}\chi\,\beta_A -2\omega\,\beta_A, \label{eq:b2}\\[0.8ex] \nabla_4\nu_{ABC} ={}&-2\nabla_{[A}\alpha_{B]C} -(2\zeta_A+\eta_A)\alpha_{BC} +(2\zeta_B+\eta_B)\alpha_{AC} +\chi_{AC}\beta_B-\chi_{BC}\beta_A \notag\\ &\quad +\chi_A{}^D(\nu_{BDC}+\nu_{CDB}) +\chi_B{}^D\nu_{DAC} -\chi_B{}^D\nu_{CDA} -2\omega\,\nu_{ABC}, \label{eq:b3}\\[0.8ex] \nabla_3\nu_{ABC} ={}&-\nabla_A(\tau_{BC}+\sigma_{BC}) +\nabla_B(\tau_{AC}+\sigma_{AC}) -\underline\eta_A(\tau_{BC}+\sigma_{BC}) +\underline\eta_B(\tau_{AC}+\sigma_{AC}) \notag\\ &\quad +2\underline\eta_C\sigma_{AB} +2\underline\omega\,\nu_{ABC} +2\underline\eta^D R_{ABCD} +\chi_{AC}\underline\beta_B-\chi_{BC}\underline\beta_A \notag\\ &\quad +\underline\chi_A{}^D\nu_{BDC} +\underline\chi_B{}^D\nu_{DAC} +\chi_A{}^D\underline\nu_{CDB} -\chi_B{}^D\underline\nu_{CDA}, \label{eq:b4}\\[0.8ex] \nabla_4R_{ABCD} ={}&-\nabla_A\nu_{CDB}+\nabla_B\nu_{CDA} -(2\zeta_A+\eta_A)\nu_{CDB} +(2\zeta_B+\eta_B)\nu_{CDA} -\eta_C\nu_{ABD}+\eta_D\nu_{ABC} \notag\\ &\quad +\chi_A{}^E R_{BECD}+\chi_B{}^E R_{EACD} -\tfrac12\chi_{AC}(\tau_{DB}+\sigma_{DB}) +\tfrac12\chi_{AD}(\tau_{CB}+\sigma_{CB}) \notag\\ &\quad +\tfrac12\chi_{BC}(\tau_{DA}+\sigma_{DA}) -\tfrac12\chi_{BD}(\tau_{CA}+\sigma_{CA}) -\tfrac12\underline\chi_{AC}\alpha_{BD} +\tfrac12\underline\chi_{AD}\alpha_{BC} \notag\\ &\quad +\tfrac12\underline\chi_{BC}\alpha_{AD} -\tfrac12\underline\chi_{BD}\alpha_{AC}, \label{eq:b5}\\[0.8ex] \nabla_4\sigma_{AB} ={}&\nabla^C\nu_{ABC} +(\zeta^C+\eta^C)\nu_{ABC} -{\text{tr}}\chi\,\sigma_{AB} +\eta_B\beta_A-\eta_A\beta_B \notag\\ &\quad +\tfrac12\chi_A{}^C(\tau_{BC}+\sigma_{BC}) -\tfrac12\chi_B{}^C(\tau_{AC}+\sigma_{AC}) +\tfrac12\underline\chi_A{}^C\alpha_{CB} -\tfrac12\underline\chi_B{}^C\alpha_{CA}, \label{eq:b6}\\[0.8ex] \nabla_3R_{ABCD} ={}&-\nabla_A\underline\nu_{CDB}+\nabla_B\underline\nu_{CDA} +(\zeta_A-\underline\eta_A)\underline\nu_{CDB} -(\zeta_B-\underline\eta_B)\underline\nu_{CDA} \notag\\ &\quad -\underline\eta_C\underline\nu_{ABD}+\underline\eta_D\underline\nu_{ABC} +\underline\chi_A{}^E R_{BECD}+\underline\chi_B{}^E R_{EACD} -\tfrac12\chi_{AC}\underline\alpha_{BD} \notag\\ &\quad +\tfrac12\chi_{AD}\underline\alpha_{BC} +\tfrac12\chi_{BC}\underline\alpha_{AD} -\tfrac12\chi_{BD}\underline\alpha_{AC} -\tfrac12\underline\chi_{AC}(\tau_{BD}+\sigma_{BD}) \notag\\ &\quad +\tfrac12\underline\chi_{AD}(\tau_{BC}+\sigma_{BC}) +\tfrac12\underline\chi_{BC}(\tau_{AD}+\sigma_{AD}) -\tfrac12\underline\chi_{BD}(\tau_{AC}+\sigma_{AC}), \label{eq:b7}\\[0.8ex] \nabla_3\tau_{AB} ={}&-2\underline\chi^{CD}R_{CADB} +\gamma^{CD}\Bigl[ -\nabla_C\underline\nu_{DBA}+\nabla_A\underline\nu_{DBC} +(\zeta_C-\underline\eta_C)\underline\nu_{DBA} -(\zeta_A-\underline\eta_A)\underline\nu_{DBC} \notag\\ &\qquad\qquad -\underline\eta_D\underline\nu_{CAB}+\underline\eta_B\underline\nu_{CAD} +\underline\chi_C{}^E R_{AEDB}+\underline\chi_A{}^E R_{ECDB} -\tfrac12\chi_{CD}\underline\alpha_{AB} \notag\\ &\qquad\qquad +\tfrac12\chi_{CB}\underline\alpha_{AD} +\tfrac12\chi_{AD}\underline\alpha_{BC} -\tfrac12\chi_{AB}\underline\alpha_{CD} -\tfrac12\underline\chi_{CD}(\tau_{AB}+\sigma_{AB}) \notag\\ &\qquad\qquad +\tfrac12\underline\chi_{CB}(\tau_{AD}+\sigma_{AD}) +\tfrac12\underline\chi_{AD}(\tau_{CB}+\sigma_{CB}) -\tfrac12\underline\chi_{AB}(\tau_{CD}+\sigma_{CD}) \Bigr], \label{eq:b8}\\[0.8ex] \nabla_3\rho ={}&-\frac12\gamma^{AB}\nabla_3\tau_{AB}, \label{eq:b9}\\[0.8ex] \nabla_3\sigma_{AB} ={}&-\nabla^C\underline\nu_{ABC} +(\zeta^C-\underline\eta^C)\underline\nu_{ABC} -{\text{tr}}\underline\chi\,\sigma_{AB} -\underline\eta_A\underline\beta_B+\underline\eta_B\underline\beta_A \notag\\ &\quad -\tfrac12\chi_A{}^C\underline\alpha_{CB} +\tfrac12\chi_B{}^C\underline\alpha_{CA} -\tfrac12\underline\chi_A{}^C(\tau_{CB}+\sigma_{CB}) +\tfrac12\underline\chi_B{}^C(\tau_{CA}+\sigma_{CA}), \label{eq:b10}\\[0.8ex] \nabla_4\underline\nu_{ABC} ={}&-\nabla_A(\tau_{CB}+\sigma_{CB}) +\nabla_B(\tau_{CA}+\sigma_{CA}) -\eta_A(\tau_{CB}+\sigma_{CB}) +\eta_B(\tau_{CA}+\sigma_{CA}) \notag\\ &\quad -2\eta_C\sigma_{AB} +2\omega\,\underline\nu_{ABC} +2\eta^D R_{ABCD} +\chi_A{}^D\underline\nu_{BDC} +\chi_B{}^D\underline\nu_{DAC} \notag\\ &\quad -\underline\chi_{AC}\beta_B+\underline\chi_{BC}\beta_A +\underline\chi_A{}^D\nu_{CDB} -\underline\chi_B{}^D\nu_{CDA}, \label{eq:b11}\\[0.8ex] \nabla_3\underline\nu_{ABC} ={}&-2\nabla_{[A}\underline\alpha_{B]C} +(2\zeta_A-\underline\eta_A)\underline\alpha_{BC} -(2\zeta_B-\underline\eta_B)\underline\alpha_{AC} -2\underline\omega\,\underline\nu_{ABC} \notag\\ &\quad -\underline\chi_{AC}\underline\beta_B+\underline\chi_{BC}\underline\beta_A +\underline\chi_A{}^D(\underline\nu_{BDC}+\underline\nu_{CDB}) +\underline\chi_B{}^D\underline\nu_{DAC} -\underline\chi_B{}^D\underline\nu_{CDA}, \label{eq:b12}\\[0.8ex] \nabla_3\underline\beta_A ={}&-\nabla^B\underline\alpha_{BA} +(2\zeta^B-\underline\eta^B)\underline\alpha_{BA} +\hat{\underline\chi}^{BC}\underline\nu_{ABC} -\hat{\underline\chi}_A{}^B\underline\beta_B \notag\\ &\quad -{\text{tr}}\underline\chi\,\underline\beta_A -2\underline\omega\,\underline\beta_A, \label{eq:b13}\\[0.8ex] \nabla_4\underline\alpha_{AB} ={}&4\omega\,\underline\alpha_{AB} -2\eta^C\underline\nu_{C(AB)} -2\eta_{(A}\underline\beta_{B)} -\nabla_3\tau_{AB} \notag\\ &\quad +2{\text{Sym}}_{AB}\Bigl[ -\nabla^C\underline\nu_{CAB}+\zeta^C\underline\nu_{CAB} -\tfrac12{\text{tr}}\chi\,\underline\alpha_{AB} -\tfrac12{\text{tr}}\underline\chi\,\tau_{AB} \notag\\ &\qquad\qquad +\tfrac12\chi_A{}^C\underline\alpha_{CB} +\tfrac12\underline\chi_A{}^C(\tau_{BC}+\sigma_{BC}) -\underline\chi^{CD}R_{CADB} -\underline\chi_B{}^C\sigma_{CA} \Bigr]. \label{eq:b14} \end{align} \]
Below is the mathematica test for \(\nabla_4\beta,\nabla_3\underline\beta\), \(\nabla_4\nu,\nabla_3\nu\), \(\nabla_4\sigma,\nabla_4\tau\). It should be 100% success rate.
ClearAll["Global`*"];
MakeVec[d_Integer, prefix_String] :=
Table[Symbol[prefix <> ToString[i]], {i, d}];
MakeSymMat[d_Integer, prefix_String] :=
Table[Symbol[prefix <> ToString[Min[i,j]] <> ToString[Max[i,j]]],
{i, d}, {j, d}];
MakeAntisymMat[d_Integer, prefix_String] :=
Table[
Which[i == j, 0,
i < j, Symbol[prefix <> ToString[i] <> ToString[j]],
True, -Symbol[prefix <> ToString[j] <> ToString[i]]
],
{i, d}, {j, d}];
(* Generic matrix (no symmetry) *)
MakeGenMat[d_Integer, prefix_String] :=
Table[Symbol[prefix <> ToString[i] <> ToString[j]], {i, d}, {j, d}];
(* 3-tensor nu_{ABC}: antisymmetric in first two indices, free in third *)
MakeNu[d_Integer, prefix_String] :=
Table[
Which[a == b, 0,
a < b, Symbol[prefix <> ToString[a] <> ToString[b] <> ToString[c]],
True, -Symbol[prefix <> ToString[b] <> ToString[a] <> ToString[c]]
],
{a, d}, {b, d}, {c, d}];
(* 4-tensor R_{ABCD}: antisymmetric in (A,B), antisymmetric in (C,D),
symmetric under pair swap (AB)<->(CD).
Independent components: (A<B, C<D) with (A,B) <= (C,D) lexicographically,
but for simplicity we just enforce antisymmetry in each pair
and pair-swap symmetry. *)
MakeRiem[d_Integer, prefix_String] :=
Module[{symb, tab},
symb[a_, b_, c_, dd_] /; a > b := -symb[b, a, c, dd];
symb[a_, b_, c_, dd_] /; c > dd := -symb[a, b, dd, c];
symb[a_, b_, c_, dd_] /; {a, b} == {c, dd} && a == b := 0;
symb[a_, b_, c_, dd_] /; a == b := 0;
symb[a_, b_, c_, dd_] /; c == dd := 0;
(* pair-swap: R_{abcd} = R_{cdab} *)
symb[a_, b_, c_, dd_] /; OrderedQ[{{c, dd}, {a, b}}] && {a, b} =!= {c, dd} :=
symb[c, dd, a, b];
(* base case *)
symb[a_, b_, c_, dd_] /; a < b && c < dd && OrderedQ[{{a, b}, {c, dd}}] :=
Symbol[prefix <> ToString[a] <> ToString[b] <> ToString[c] <> ToString[dd]];
Table[symb[a, b, c, dd], {a, d}, {b, d}, {c, d}, {dd, d}]
];
TFPart[m_] := Module[{s = (m + Transpose[m])/2, nn = Length[m]},
Simplify[s - Tr[s]/nn IdentityMatrix[nn]]
];
dims = {2, 3, 4};
betaHatTests = Flatten @ Table[
Module[
{
chi = MakeSymMat[d, "chiH" <> ToString[d]],
nu = MakeNu[d, "nuH" <> ToString[d]],
chiHat, trchi, beta, rawTerms, hatTerms
},
trchi = Tr[chi];
chiHat = TFPart[chi];
(* beta_A = gamma^{BC} nu_{ABC} = Sum_B nu[[A,B,B]] *)
beta = Table[Sum[nu[[a, b, b]], {b, d}], {a, d}];
(* Raw lower-order terms (without the minus signs and the leading terms): *)
(* chi_A^B beta_B + chi^{BC} nu_{ABC} + trchi beta_A *)
rawTerms = Table[
Sum[chi[[a, b]] * beta[[b]], {b, d}]
+ Sum[chi[[b, c]] * nu[[a, b, c]], {b, d}, {c, d}]
+ trchi * beta[[a]],
{a, d}
];
(* Hat form: hat_chi_A^B beta_B + hat_chi^{BC} nu_{ABC} + (1+2/n) trchi beta_A *)
hatTerms = Table[
Sum[chiHat[[a, b]] * beta[[b]], {b, d}]
+ Sum[chiHat[[b, c]] * nu[[a, b, c]], {b, d}, {c, d}]
+ (1 + 2/d) * trchi * beta[[a]],
{a, d}
];
{
VerificationTest[
Simplify[rawTerms - hatTerms],
ConstantArray[0, d],
TestID -> "beta4: raw-to-hat conversion, n=" <> ToString[d]
]
}
],
{d, dims}
];
betabarHatTests = Flatten @ Table[
Module[
{
chib = MakeSymMat[d, "chibH" <> ToString[d]],
nub = MakeNu[d, "nubH" <> ToString[d]],
chibHat, trchib, betab, rawTerms, hatTerms
},
trchib = Tr[chib];
chibHat = TFPart[chib];
(* betabar_A = gamma^{BC} nubar_{ABC} = Sum_B nub[[A,B,B]] *)
betab = Table[Sum[nub[[a, b, b]], {b, d}], {a, d}];
(* Raw: chibar^{BC} nubar_{ABC} - chibar_A^B betabar_B - trchibar betabar_A *)
rawTerms = Table[
Sum[chib[[b, c]] * nub[[a, b, c]], {b, d}, {c, d}]
- Sum[chib[[a, b]] * betab[[b]], {b, d}]
- trchib * betab[[a]],
{a, d}
];
(* Hat: hat_chibar^{BC} nubar_{ABC} - hat_chibar_A^B betabar_B - trchibar betabar_A *)
hatTerms = Table[
Sum[chibHat[[b, c]] * nub[[a, b, c]], {b, d}, {c, d}]
- Sum[chibHat[[a, b]] * betab[[b]], {b, d}]
- trchib * betab[[a]],
{a, d}
];
{
VerificationTest[
Simplify[rawTerms - hatTerms],
ConstantArray[0, d],
TestID -> "betabar3: raw-to-hat conversion, n=" <> ToString[d]
]
}
],
{d, dims}
];
nu4DerivTests = Flatten @ Table[
Module[
{
chi = MakeSymMat[d, "chiN4" <> ToString[d]],
alpha = MakeSymMat[d, "alN4" <> ToString[d]],
nu = MakeNu[d, "nuN4" <> ToString[d]],
beta = MakeVec[d, "beN4" <> ToString[d]],
zeta = MakeVec[d, "zeN4" <> ToString[d]],
eta = MakeVec[d, "etN4" <> ToString[d]],
om = Symbol["omN4" <> ToString[d]],
(* The three D-terms expanded, with nabla_4 nu on the LHS *)
(* What remains on the RHS after moving nabla_4 nu_{ABC} to the left *)
sumDADB, stated
},
(* D_4 R_{ABC4} contributes (after moving nabla_4 nu to LHS):
eta_A alpha_{BC} - eta_B alpha_{AC} + 2 omega nu_{ABC} *)
(* D_A R_{B4C4} contributes:
nabla_A alpha_{BC} + 2 zeta_A alpha_{BC} - chi_{AB} beta_C - chi_{AC} beta_B
- chi_A^D nu_{BDC} - chi_A^D nu_{CDB} *)
(* D_B R_{4AC4} contributes:
-nabla_B alpha_{AC} - 2 zeta_B alpha_{AC} + chi_{BA} beta_C + chi_{BC} beta_A
- chi_B^D nu_{DAC} + chi_B^D nu_{CDA} *)
(* Bianchi: D_4 R + D_A R + D_B R = 0, so RHS = -(D_4 remainder + D_A + D_B) *)
sumDADB[a_, b_, c_] :=
(* From D_4 R_{ABC4}: *)
eta[[a]] * alpha[[b, c]] - eta[[b]] * alpha[[a, c]] + 2 om * nu[[a, b, c]]
(* From D_A R_{B4C4}: *)
+ 2 zeta[[a]] * alpha[[b, c]]
- chi[[a, b]] * beta[[c]] - chi[[a, c]] * beta[[b]]
- Sum[chi[[a, dd]] * nu[[b, dd, c]], {dd, d}]
- Sum[chi[[a, dd]] * nu[[c, dd, b]], {dd, d}]
(* From D_B R_{4AC4}: *)
- 2 zeta[[b]] * alpha[[a, c]]
+ chi[[b, a]] * beta[[c]] + chi[[b, c]] * beta[[a]]
- Sum[chi[[b, dd]] * nu[[dd, a, c]], {dd, d}]
+ Sum[chi[[b, dd]] * nu[[c, dd, a]], {dd, d}];
(* The stated equation (eq nu4-explicit), RHS with nabla terms removed:
-(2 zeta_A + eta_A) alpha_{BC} + (2 zeta_B + eta_B) alpha_{AC}
+ chi_{AC} beta_B - chi_{BC} beta_A
+ chi_A^D (nu_{BDC} + nu_{CDB}) + chi_B^D nu_{DAC} - chi_B^D nu_{CDA}
- 2 omega nu_{ABC} *)
stated[a_, b_, c_] :=
-(2 zeta[[a]] + eta[[a]]) * alpha[[b, c]]
+ (2 zeta[[b]] + eta[[b]]) * alpha[[a, c]]
+ chi[[a, c]] * beta[[b]] - chi[[b, c]] * beta[[a]]
+ Sum[chi[[a, dd]] * (nu[[b, dd, c]] + nu[[c, dd, b]]), {dd, d}]
+ Sum[chi[[b, dd]] * nu[[dd, a, c]], {dd, d}]
- Sum[chi[[b, dd]] * nu[[c, dd, a]], {dd, d}]
- 2 om * nu[[a, b, c]];
(* The Bianchi identity says D_4 R + D_A R + D_B R = 0,
i.e., nabla_4 nu_{ABC} + (sumDADB) = 0.
So nabla_4 nu_{ABC} = -(sumDADB).
The stated equation says nabla_4 nu_{ABC} = (stated terms) + derivative terms.
Ignoring the derivative terms (nabla_A alpha etc.) which pass through,
we check: -(sumDADB) == stated, i.e., sumDADB + stated == 0. *)
Flatten @ Table[
If[a == b, Nothing,
VerificationTest[
Simplify[sumDADB[a, b, c] + stated[a, b, c]],
0,
TestID -> "nu4 derivation: sum matches stated (" <>
ToString[{a, b, c}] <> "), n=" <> ToString[d]
]
],
{a, d}, {b, d}, {c, d}
]
],
{d, dims}
];
nu3DerivTests = Flatten @ Table[
Module[
{
chi = MakeSymMat[d, "chiN3" <> ToString[d]],
chib = MakeSymMat[d, "chibN3" <> ToString[d]],
tau = MakeSymMat[d, "tauN3" <> ToString[d]],
sig = MakeAntisymMat[d, "sigN3" <> ToString[d]],
nu = MakeNu[d, "nuN3" <> ToString[d]],
nub = MakeNu[d, "nubN3" <> ToString[d]],
Riem = MakeRiem[d, "RN3" <> ToString[d]],
beta = MakeVec[d, "beN3" <> ToString[d]],
betab = MakeVec[d, "bebN3" <> ToString[d]],
etab = MakeVec[d, "etbN3" <> ToString[d]],
omb = Symbol["ombN3" <> ToString[d]],
(* tau+sigma combined *)
tps,
sumD3DADB, stated
},
tps[a_, b_] := tau[[a, b]] + sig[[a, b]];
(* D_3 R_{ABC4} contributes (with nabla_3 nu on LHS):
etab_A (tau_{BC}+sig_{BC}) - etab_B (tau_{AC}+sig_{AC})
- 2 etab_C sigma_{AB} - 2 omb nu_{ABC} - 2 etab^D R_{ABCD} *)
(* D_A R_{B3C4} contributes:
chibar_{AB} beta_C - chi_{AC} betabar_B
- chibar_A^D nu_{BDC} - chi_A^D nubar_{CDB} *)
(* D_B R_{3AC4} contributes:
-chibar_{BA} beta_C + chi_{BC} betabar_A
- chibar_B^D nu_{DAC} + chi_B^D nubar_{CDA} *)
sumD3DADB[a_, b_, c_] :=
etab[[a]] * tps[b, c] - etab[[b]] * tps[a, c]
- 2 etab[[c]] * sig[[a, b]]
- 2 omb * nu[[a, b, c]]
- 2 Sum[etab[[dd]] * Riem[[a, b, c, dd]], {dd, d}]
+ chib[[a, b]] * beta[[c]] - chi[[a, c]] * betab[[b]]
- Sum[chib[[a, dd]] * nu[[b, dd, c]], {dd, d}]
- Sum[chi[[a, dd]] * nub[[c, dd, b]], {dd, d}]
- chib[[b, a]] * beta[[c]] + chi[[b, c]] * betab[[a]]
- Sum[chib[[b, dd]] * nu[[dd, a, c]], {dd, d}]
+ Sum[chi[[b, dd]] * nub[[c, dd, a]], {dd, d}];
(* The stated eq (nu3-explicit), RHS without derivative terms:
-etab_A (tau_{BC}+sig_{BC}) + etab_B (tau_{AC}+sig_{AC})
+ 2 etab_C sigma_{AB} + 2 omb nu_{ABC} + 2 etab^D R_{ABCD}
+ chi_{AC} betab_B - chi_{BC} betab_A
+ chibar_A^D nu_{BDC} + chibar_B^D nu_{DAC}
+ chi_A^D nubar_{CDB} - chi_B^D nubar_{CDA} *)
stated[a_, b_, c_] :=
-etab[[a]] * tps[b, c] + etab[[b]] * tps[a, c]
+ 2 etab[[c]] * sig[[a, b]]
+ 2 omb * nu[[a, b, c]]
+ 2 Sum[etab[[dd]] * Riem[[a, b, c, dd]], {dd, d}]
+ chi[[a, c]] * betab[[b]] - chi[[b, c]] * betab[[a]]
+ Sum[chib[[a, dd]] * nu[[b, dd, c]], {dd, d}]
+ Sum[chib[[b, dd]] * nu[[dd, a, c]], {dd, d}]
+ Sum[chi[[a, dd]] * nub[[c, dd, b]], {dd, d}]
- Sum[chi[[b, dd]] * nub[[c, dd, a]], {dd, d}];
Flatten @ Table[
If[a == b, Nothing,
VerificationTest[
Simplify[sumD3DADB[a, b, c] + stated[a, b, c]],
0,
TestID -> "nu3 derivation: sum matches stated (" <>
ToString[{a, b, c}] <> "), n=" <> ToString[d]
]
],
{a, d}, {b, d}, {c, d}
]
],
{d, dims}
];
sigma4DerivTests = Flatten @ Table[
Module[
{
chi = MakeSymMat[d, "chiS4" <> ToString[d]],
chib = MakeSymMat[d, "chibS4" <> ToString[d]],
alpha = MakeSymMat[d, "alS4" <> ToString[d]],
tau = MakeSymMat[d, "tauS4" <> ToString[d]],
sig = MakeAntisymMat[d, "sigS4" <> ToString[d]],
nu = MakeNu[d, "nuS4" <> ToString[d]],
beta = MakeVec[d, "beS4" <> ToString[d]],
zeta = MakeVec[d, "zeS4" <> ToString[d]],
eta = MakeVec[d, "etS4" <> ToString[d]],
trchi,
(* D_4 R_{34AB} piece (without the nabla_4 sigma term) *)
d4piece, tangpiece, stated
},
trchi = Tr[chi];
(* -(1/2) D_4 R_{34AB} = -(1/2)(2 nabla_4 sigma - 2 eta^C nu + 2 eta_A beta_B - 2 eta_B beta_A)
= -nabla_4 sigma + eta^C nu - eta_A beta_B + eta_B beta_A
After moving nabla_4 sigma to LHS, what remains from D_4 piece: *)
d4piece[a_, b_] :=
Sum[eta[[c]] * nu[[a, b, c]], {c, d}]
- eta[[a]] * beta[[b]] + eta[[b]] * beta[[a]];
(* gamma^{CD} D_C R_{D4AB} *)
tangpiece[a_, b_] :=
Sum[zeta[[c]] * nu[[a, b, c]], {c, d}]
- trchi * sig[[a, b]]
+ (1/2) Sum[chi[[a, c]] * (tau[[b, c]] + sig[[b, c]]), {c, d}]
- (1/2) Sum[chi[[b, c]] * (tau[[a, c]] + sig[[a, c]]), {c, d}]
+ (1/2) Sum[chib[[a, c]] * alpha[[c, b]], {c, d}]
- (1/2) Sum[chib[[b, c]] * alpha[[c, a]], {c, d}];
(* stated RHS of eq sigma4-explicit (without nabla^C nu and nabla_4 sigma): *)
stated[a_, b_] :=
Sum[(zeta[[c]] + eta[[c]]) * nu[[a, b, c]], {c, d}]
- trchi * sig[[a, b]]
+ eta[[b]] * beta[[a]] - eta[[a]] * beta[[b]]
+ (1/2) Sum[chi[[a, c]] * (tau[[b, c]] + sig[[b, c]]), {c, d}]
- (1/2) Sum[chi[[b, c]] * (tau[[a, c]] + sig[[a, c]]), {c, d}]
+ (1/2) Sum[chib[[a, c]] * alpha[[c, b]], {c, d}]
- (1/2) Sum[chib[[b, c]] * alpha[[c, a]], {c, d}];
(* Check: d4piece + tangpiece == stated *)
Flatten @ Table[
If[a >= b, Nothing,
VerificationTest[
Simplify[d4piece[a, b] + tangpiece[a, b] - stated[a, b]],
0,
TestID -> "sigma4 derivation: (" <> ToString[{a, b}] <>
"), n=" <> ToString[d]
]
],
{a, d}, {b, d}
]
],
{d, dims}
];
beta4DerivTests = Flatten @ Table[
Module[
{
chi = MakeSymMat[d, "chiB4" <> ToString[d]],
alpha = MakeSymMat[d, "alB4" <> ToString[d]],
nu = MakeNu[d, "nuB4" <> ToString[d]],
beta = MakeVec[d, "beB4" <> ToString[d]],
zeta = MakeVec[d, "zeB4" <> ToString[d]],
eta = MakeVec[d, "etB4" <> ToString[d]],
om = Symbol["omB4" <> ToString[d]],
trchi,
d4piece, tangpiece, stated
},
trchi = Tr[chi];
(* -(1/2) D_4 R_{34A4} (with nabla_4 beta on LHS):
-2 omega beta_A + eta^B alpha_{BA} *)
d4piece[a_] :=
-2 om * beta[[a]] + Sum[eta[[b]] * alpha[[b, a]], {b, d}];
(* gamma^{BC} D_B R_{C4A4}: *)
tangpiece[a_] :=
2 Sum[zeta[[b]] * alpha[[b, a]], {b, d}]
- trchi * beta[[a]]
- Sum[chi[[a, b]] * beta[[b]], {b, d}]
- Sum[chi[[b, c]] * nu[[a, b, c]], {b, d}, {c, d}];
(* Stated RHS of eq beta4-explicit-raw (without nabla^B alpha and nabla_4 beta): *)
stated[a_] :=
Sum[(2 zeta[[b]] + eta[[b]]) * alpha[[b, a]], {b, d}]
- Sum[chi[[a, b]] * beta[[b]], {b, d}]
- Sum[chi[[b, c]] * nu[[a, b, c]], {b, d}, {c, d}]
- trchi * beta[[a]]
- 2 om * beta[[a]];
Table[
VerificationTest[
Simplify[d4piece[a] + tangpiece[a] - stated[a]],
0,
TestID -> "beta4 derivation: A=" <> ToString[a] <>
", n=" <> ToString[d]
],
{a, d}
]
],
{d, dims}
];
d4SigmaAntisymTests = Flatten @ Table[
Module[
{
nu = MakeNu[d, "nuAS" <> ToString[d]],
beta = MakeVec[d, "beAS" <> ToString[d]],
eta = MakeVec[d, "etAS" <> ToString[d]],
expr
},
expr[a_, b_] :=
-2 Sum[eta[[c]] * nu[[a, b, c]], {c, d}]
+ 2 eta[[a]] * beta[[b]] - 2 eta[[b]] * beta[[a]];
Flatten @ Table[
If[a >= b, Nothing,
VerificationTest[
Simplify[expr[a, b] + expr[b, a]],
0,
TestID -> "D4 sigma antisym: (" <> ToString[{a, b}] <>
"), n=" <> ToString[d]
]
],
{a, d}, {b, d}
]
],
{d, dims}
];
tau4TraceTests = Flatten @ Table[
Module[
{
chi = MakeSymMat[d, "chiT4" <> ToString[d]],
chib = MakeSymMat[d, "chibT4" <> ToString[d]],
alpha = MakeSymMat[d, "alT4" <> ToString[d]],
tau = MakeSymMat[d, "tauT4" <> ToString[d]],
sig = MakeAntisymMat[d, "sigT4" <> ToString[d]],
nu = MakeNu[d, "nuT4" <> ToString[d]],
nub = MakeNu[d, "nubT4" <> ToString[d]],
Riem = MakeRiem[d, "RT4" <> ToString[d]],
beta = MakeVec[d, "beT4" <> ToString[d]],
zeta = MakeVec[d, "zeT4" <> ToString[d]],
eta = MakeVec[d, "etT4" <> ToString[d]],
tps,
(* Lower-order terms of R4-explicit for given (A,B,C,D) *)
r4lo,
(* Lower-order terms of tau4-raw for given (A,B) *)
tau4lo,
(* gamma^{CD} r4lo(C,A,D,B) + (-2 chi^{CD} R_{CADB}) *)
traceOfR4, directTau4
},
tps[a_, b_] := tau[[a, b]] + sig[[a, b]];
(* R4-explicit lower-order terms (without nabla_A nu, nabla_B nu, nabla_4 R):
-(2 zeta_A+eta_A) nu_{CDB} + (2 zeta_B+eta_B) nu_{CDA}
-eta_C nu_{ABD} + eta_D nu_{ABC}
+ chi_A^E R_{BECD} + chi_B^E R_{EACD}
-(1/2) chi_{AC} tps_{DB} + (1/2) chi_{AD} tps_{CB}
+(1/2) chi_{BC} tps_{DA} - (1/2) chi_{BD} tps_{CA}
-(1/2) chibar_{AC} alpha_{BD} + (1/2) chibar_{AD} alpha_{BC}
+(1/2) chibar_{BC} alpha_{AD} - (1/2) chibar_{BD} alpha_{AC} *)
r4lo[a_, b_, c_, dd_] :=
-(2 zeta[[a]] + eta[[a]]) * nu[[c, dd, b]]
+ (2 zeta[[b]] + eta[[b]]) * nu[[c, dd, a]]
- eta[[c]] * nu[[a, b, dd]] + eta[[dd]] * nu[[a, b, c]]
+ Sum[chi[[a, e]] * Riem[[b, e, c, dd]], {e, d}]
+ Sum[chi[[b, e]] * Riem[[e, a, c, dd]], {e, d}]
- (1/2) chi[[a, c]] * tps[dd, b]
+ (1/2) chi[[a, dd]] * tps[c, b]
+ (1/2) chi[[b, c]] * tps[dd, a]
- (1/2) chi[[b, dd]] * tps[c, a]
- (1/2) chib[[a, c]] * alpha[[b, dd]]
+ (1/2) chib[[a, dd]] * alpha[[b, c]]
+ (1/2) chib[[b, c]] * alpha[[a, dd]]
- (1/2) chib[[b, dd]] * alpha[[a, c]];
(* Trace of R4: gamma^{CD} r4lo(C, A, D, B) *)
traceOfR4[a_, b_] :=
Sum[r4lo[c, a, dd, b], {c, d}, {dd, d}] (* gamma^{CD} R4_{CADB} *)
- 2 Sum[chi[[c, dd]] * Riem[[c, a, dd, b]], {c, d}, {dd, d}];
(* tau4-raw lower-order terms (without nabla and nabla_4 tau):
-2 chi^{CD} R_{CADB}
+ gamma^{CD}[
-(2 zeta_C+eta_C) nu_{DBA} + (2 zeta_A+eta_A) nu_{DBC}
-eta_D nu_{CAB} + eta_B nu_{CAD}
+chi_C^E R_{AEDB} + chi_A^E R_{ECDB}
-(1/2) chi_{CD} tps_{BA} + (1/2) chi_{CB} tps_{DA}
+(1/2) chi_{AD} tps_{BC} - (1/2) chi_{AB} tps_{DC}
-(1/2) chibar_{CD} alpha_{AB} + (1/2) chibar_{CB} alpha_{AD}
+(1/2) chibar_{AD} alpha_{BC} - (1/2) chibar_{AB} alpha_{CD}
] *)
tau4lo[a_, b_] :=
-2 Sum[chi[[c, dd]] * Riem[[c, a, dd, b]], {c, d}, {dd, d}]
+ Sum[
-(2 zeta[[c]] + eta[[c]]) * nu[[dd, b, a]]
+ (2 zeta[[a]] + eta[[a]]) * nu[[dd, b, c]]
- eta[[dd]] * nu[[c, a, b]] + eta[[b]] * nu[[c, a, dd]]
+ Sum[chi[[c, e]] * Riem[[a, e, dd, b]], {e, d}]
+ Sum[chi[[a, e]] * Riem[[e, c, dd, b]], {e, d}]
- (1/2) chi[[c, dd]] * tps[b, a]
+ (1/2) chi[[c, b]] * tps[dd, a]
+ (1/2) chi[[a, dd]] * tps[b, c]
- (1/2) chi[[a, b]] * tps[dd, c]
- (1/2) chib[[c, dd]] * alpha[[a, b]]
+ (1/2) chib[[c, b]] * alpha[[a, dd]]
+ (1/2) chib[[a, dd]] * alpha[[b, c]]
- (1/2) chib[[a, b]] * alpha[[c, dd]],
{c, d}, {dd, d}
];
Table[
VerificationTest[
Simplify[traceOfR4[a, b] - tau4lo[a, b]],
0,
TestID -> "tau4 trace consistency: (" <> ToString[{a, b}] <>
"), n=" <> ToString[d]
],
{a, d}, {b, d}
]
],
{d, {2, 3}}
];
allTests = Join[
betaHatTests,
betabarHatTests,
nu4DerivTests,
nu3DerivTests,
sigma4DerivTests,
beta4DerivTests,
d4SigmaAntisymTests,
tau4TraceTests
];
TestReport[allTests]