The conformal direction of superspace is timelike

Read-back of WheelerDeWittSuperspace.superQuad_conformal_neg.

Binders and hypotheses. The statement has exactly two inputs, and nothing else is quantified:

• an arbitrary real $3\times 3$ matrix $m = (m_{ab})_{a,b\in\{0,1,2\}}$;
• a hypothesis that $m$ is positive definite, in Mathlib's sense. This means (i) $m$ is symmetric ($m^{\mathsf T} = m$, i.e. Hermitian over $\mathbb R$), and (ii) $\sum_{i,j} x_i\, m_{ij}\, x_j > 0$ for every nonzero vector $x \in \mathbb R^3$ (Mathlib states this for finitely supported vectors, which here is all of $\mathbb R^3$).

There are no physical constants, sites, configurations or wavefunctions. Only the single matrix $m$ appears.

Conclusion. The statement asserts the strict inequality

Here $m^{-1}$ is Mathlib's matrix inverse. In general this is $(\det m)^{-1}\operatorname{adj}(m)$ when $\det m$ is a unit and the zero matrix otherwise. Positive definiteness forces $\det m > 0$, so here $m^{-1}$ is the genuine two-sided inverse. The quadratic form $\mathcal G_m(p,p)$ (the definition superQuad) is defined for any real $3\times3$ matrix $p = (p^{ab})$ as the full quadruple sum

with coefficients (the definition deWitt)

In this formula, $\sqrt{\det m}$ (the definition volume) is Mathlib's real square root Real.sqrt, which returns $0$ on negative arguments. Division is real division, with the convention $x/0 = 0$. Under the hypothesis $\det m > 0$, so the denominator $2\sqrt{\det m}$ is strictly positive and neither junk convention is triggered.

Substituting $p = m^{-1}$, so that $p^{ab} = (m^{-1})_{ab}$, the claim reads

The same matrix $m$ serves both as the metric in the coefficients and, inverted, as the "momentum" argument. The inverse enters with the index order $(m^{-1})_{ab}$ exactly as written, with no transposition. Since $m$ is symmetric, $m^{-1}$ is symmetric as well.

Edge cases and vacuity.

• The dimension is fixed at $3$; there is no varying size and no empty case.
• The hypothesis is satisfiable, for example by the identity matrix $m = I_3$. For $m = I_3$ the claim specialises to $\tfrac12\sum_{a,b,c,d}(\delta_{ac}\delta_{bd}+\delta_{ad}\delta_{bc}-\delta_{ab}\delta_{cd})\,\delta_{ab}\,\delta_{cd} < 0$. So the statement is not vacuous.
• Non-symmetric or indefinite matrices are excluded by the hypothesis, so the junk values of Real.sqrt, of division by zero and of the inverse of a singular matrix never arise within the statement's scope.
• The conclusion is a strict inequality ($<0$), not $\le 0$.