a field-theory motivated approach to computer algebra

# A higher-derivative Bianchi identity

The identity which we will prove here comes from appendix A of hep-th/0111128. It shows that a particular cubic polynomial of Weyl tensors vanishes by virtue of the Weyl tensor multi-term symmetries. The declaration of the indices, Weyl tensor and covariant derivative is done with:
{i,j,m,n,k,p,q,l,r,r#}::Indices(vector). C_{m n p q}::WeylTensor. \nabla{#}::Derivative. \nabla_{r}{ C_{m n p q} }::SatisfiesBianchi. \delta_{i j}::KroneckerDelta. Eij:=- C_{i m k l} C_{j p k q} C_{l p m q} + 1/4 C_{i m k l} C_{j m p q} C_{k l p q} - 1/2 C_{i k j l} C_{k m p q} C_{l m p q}: E:= C_{j m n k} C_{m p q n} C_{p j k q} + 1/2 C_{j k m n} C_{p q m n} C_{j k p q}: exp:= \nabla_{i}{\nabla_{j}{ @(Eij) }} - 1/6 \nabla_{i}{\nabla_{i}{ @(E) }};
$$\displaystyle{}-C_{i m k l} C_{j p k q} C_{l p m q}% +\frac{1}{4}C_{i m k l} C_{j m p q} C_{k l p q}% - \frac{1}{2}C_{i k j l} C_{k m p q} C_{l m p q}$$
$$\displaystyle{}\nabla_{i}\left(\nabla_{j}\left(-C_{i m k l} C_{j p k q} C_{l p m q}% +\frac{1}{4}C_{i m k l} C_{j m p q} C_{k l p q}% - \frac{1}{2}C_{i k j l} C_{k m p q} C_{l m p q}\right)\right)% - \frac{1}{6}\nabla_{i}\left(\nabla_{i}\left(C_{j m n k} C_{m p q n} C_{p j k q}% +\frac{1}{2}C_{j k m n} C_{p q m n} C_{j k p q}\right)\right)$$
First apply the product rule twice to write out derivatives:
distribute(_); product_rule(_); distribute(_); product_rule(_) sort_product(_); canonicalise(_) rename_dummies(_);
$$\displaystyle{}C_{i j m n} C_{i k m p} \nabla_{q}\left(\nabla_{j}{C_{n k p q}}\right)% -C_{i j m n} \nabla_{k}{C_{i p m q}} \nabla_{p}{C_{j q n k}}% -2C_{i j m n} \nabla_{i}{C_{m k p q}} \nabla_{p}{C_{j k n q}}% -C_{i j m n} \nabla_{k}{C_{i k m p}} \nabla_{q}{C_{j p n q}}% +C_{i j m n} C_{i k m p} \nabla_{j}\left(\nabla_{q}{C_{n k p q}}\right)% -2C_{i j m n} \nabla_{i}{C_{j k m p}} \nabla_{q}{C_{n k p q}}% -C_{i j m n} C_{i k p q} \nabla_{m}\left(\nabla_{p}{C_{j q n k}}\right)% - \frac{1}{4}C_{i j m n} C_{i j k p} \nabla_{q}\left(\nabla_{m}{C_{n q k p}}\right)% +\frac{1}{4}C_{i j m n} \nabla_{k}{C_{i j p q}} \nabla_{p}{C_{m n k q}}% - \frac{1}{2}C_{i j m n} \nabla_{i}{C_{j k p q}} \nabla_{k}{C_{m n p q}}% - \frac{1}{4}C_{i j m n} \nabla_{k}{C_{i j k p}} \nabla_{q}{C_{m n p q}}% - \frac{1}{4}C_{i j m n} C_{i j k p} \nabla_{m}\left(\nabla_{q}{C_{n q k p}}\right)% - \frac{1}{2}C_{i j m n} \nabla_{i}{C_{m n k p}} \nabla_{q}{C_{j q k p}}% +\frac{1}{4}C_{i j m n} C_{i k p q} \nabla_{j}\left(\nabla_{k}{C_{m n p q}}\right)% - \frac{1}{2}C_{i j m n} C_{i j m k} \nabla_{p}\left(\nabla_{q}{C_{n p k q}}\right)% +C_{i j m n} \nabla_{k}{C_{i j m p}} \nabla_{q}{C_{n q k p}}% -C_{i j m n} \nabla_{k}{C_{i j m p}} \nabla_{q}{C_{n k p q}}% +\frac{1}{2}C_{i j m n} C_{i k p q} \nabla_{m}\left(\nabla_{j}{C_{n k p q}}\right)% +\frac{1}{2}C_{i j m n} \nabla_{i}{C_{m k p q}} \nabla_{n}{C_{j k p q}}% - \frac{1}{2}C_{i j m n} \nabla_{i}{C_{j k p q}} \nabla_{m}{C_{n k p q}}% +\frac{1}{2}C_{i j m n} C_{i k p q} \nabla_{j}\left(\nabla_{m}{C_{n k p q}}\right)% +\frac{1}{2}C_{i j m n} C_{i k m p} \nabla_{q}\left(\nabla_{q}{C_{j k n p}}\right)% +C_{i j m n} \nabla_{k}{C_{i p m q}} \nabla_{k}{C_{j p n q}}% - \frac{1}{4}C_{i j m n} C_{i j k p} \nabla_{q}\left(\nabla_{q}{C_{m n k p}}\right)% - \frac{1}{2}C_{i j m n} \nabla_{k}{C_{i j p q}} \nabla_{k}{C_{m n p q}}$$
Because the identity which we intend to prove is only supposed to hold on Einstein spaces, we set the divergence of the Weyl tensor to zero,
substitute(_, $\nabla_{i}{ C_{k i l m} } -> 0, \nabla_{i}{ C_{k m l i} } -> 0$);
$$\displaystyle{}C_{i j m n} C_{i k m p} \nabla_{q}\left(\nabla_{j}{C_{n k p q}}\right)% -C_{i j m n} \nabla_{k}{C_{i p m q}} \nabla_{p}{C_{j q n k}}% -2C_{i j m n} \nabla_{i}{C_{m k p q}} \nabla_{p}{C_{j k n q}}% -C_{i j m n} C_{i k p q} \nabla_{m}\left(\nabla_{p}{C_{j q n k}}\right)% - \frac{1}{4}C_{i j m n} C_{i j k p} \nabla_{q}\left(\nabla_{m}{C_{n q k p}}\right)% +\frac{1}{4}C_{i j m n} \nabla_{k}{C_{i j p q}} \nabla_{p}{C_{m n k q}}% - \frac{1}{2}C_{i j m n} \nabla_{i}{C_{j k p q}} \nabla_{k}{C_{m n p q}}% +\frac{1}{4}C_{i j m n} C_{i k p q} \nabla_{j}\left(\nabla_{k}{C_{m n p q}}\right)% +\frac{1}{2}C_{i j m n} C_{i k p q} \nabla_{m}\left(\nabla_{j}{C_{n k p q}}\right)% +\frac{1}{2}C_{i j m n} \nabla_{i}{C_{m k p q}} \nabla_{n}{C_{j k p q}}% - \frac{1}{2}C_{i j m n} \nabla_{i}{C_{j k p q}} \nabla_{m}{C_{n k p q}}% +\frac{1}{2}C_{i j m n} C_{i k p q} \nabla_{j}\left(\nabla_{m}{C_{n k p q}}\right)% +\frac{1}{2}C_{i j m n} C_{i k m p} \nabla_{q}\left(\nabla_{q}{C_{j k n p}}\right)% +C_{i j m n} \nabla_{k}{C_{i p m q}} \nabla_{k}{C_{j p n q}}% - \frac{1}{4}C_{i j m n} C_{i j k p} \nabla_{q}\left(\nabla_{q}{C_{m n k p}}\right)% - \frac{1}{2}C_{i j m n} \nabla_{k}{C_{i j p q}} \nabla_{k}{C_{m n p q}}$$
This expression should vanish upon use of the Bianchi identity. By expanding all tensors using their Young projectors, this becomes manifest; a few seconds of computation produces:
young_project_product(_);
$$\displaystyle{}0$$
This proves the identity.