Inverse DeWitt supermetric on symmetric tensors

Read-back of WheelerDeWittSuperspace.invSuperMap_superMap.

Variables and hypotheses. Let $m = (m_{ab})$ and $p = (p^{ab})$ be arbitrary real $3\times 3$ matrices, with indices $a,b,c,d \in \{0,1,2\}$. The statement assumes exactly two hypotheses:

• $m$ is positive definite in Mathlib's sense. This means $m$ is symmetric ($m^\top = m$, which is the Hermitian condition over $\mathbb{R}$) and $\sum_{i,j} x_i\, m_{ij}\, x_j > 0$ for every nonzero $x \in \mathbb{R}^3$.
• $p$ is symmetric, $p^\top = p$.

No other conditions are imposed. In particular, the trace of $p$ is unrestricted, and no condition is placed on $m$ beyond positive definiteness. The hypotheses are satisfiable, for example by $m = I$ and $p = 0$, so the statement is not vacuous.

Definitions used, unfolded. Write $h = \det m$ and $\sqrt{h}$ for the real square root of $\det m$. Under the hypothesis on $m$, $\det m > 0$, so $\sqrt{h} > 0$, $m$ is invertible, and $m^{-1}$ is the genuine matrix inverse. (Outside this hypothesis, the code's square root and inverse would return $0$ by convention; that case is excluded here.) Write $m^{ab}$ for the $(a,b)$ entry of $m^{-1}$.

• The DeWitt supermetric is

$$G_{abcd}(m) = \frac{m_{ac}\,m_{bd} + m_{ad}\,m_{bc} - m_{ab}\,m_{cd}}{2\sqrt{\det m}}.$$

• The inverse supermetric is

$$G^{abcd}(m) = \frac{\sqrt{\det m}\,\bigl(m^{ac}\,m^{bd} + m^{ad}\,m^{bc} - 2\,m^{ab}\,m^{cd}\bigr)}{2}.$$

• The index lowering map sends a matrix $p$ to the matrix

$$\bigl(\mathcal{G}_m(p)\bigr)_{ab} = \sum_{c=0}^{2}\sum_{d=0}^{2} G_{abcd}(m)\,p^{cd}.$$

• The index raising map sends a matrix $k$ to the matrix

$$\bigl(\mathcal{G}^{-1}_m(k)\bigr)^{ab} = \sum_{c=0}^{2}\sum_{d=0}^{2} G^{abcd}(m)\,k_{cd}.$$

Both maps are defined on all real $3\times 3$ matrices, symmetric or not, and the sums run over all nine ordered pairs $(c,d)$.

Assertion. For every such $m$ and $p$, applying index lowering and then index raising returns $p$ exactly, entrywise:

$$\mathcal{G}^{-1}_m\bigl(\mathcal{G}_m(p)\bigr) = p,$$

that is, for all $a,b$,

$$\sum_{c,d} G^{abcd}(m) \sum_{e,f} G_{cdef}(m)\, p^{ef} = p^{ab}.$$

This is a one-sided statement. It asserts only that raising undoes lowering, and only on symmetric $p$. It says nothing about the reverse composition $\mathcal{G}_m(\mathcal{G}^{-1}_m(k))$, and nothing about non-symmetric inputs. The identity is an equality of real matrices, with no limit or approximation involved.