DeWitt's intrinsic time: superspace fibre is a Lorentzian cone

Read-back of WheelerDeWittSuperspace.velocityQuad_cone.

Data and hypotheses. The statement is universally quantified over:

• two arbitrary real $3\times 3$ matrices $\hat h$ (the code's mh) and $\delta$ (the code's dh);
• two real numbers $s$ and $\dot s$ (the code's s and ds).

It assumes exactly the following:

1. $\hat h$ is positive definite in Mathlib's sense. This means $\hat h$ is symmetric ($\hat h^{T}=\hat h$) and $v^{T}\hat h\,v>0$ for every nonzero $v\in\mathbb R^3$.
2. $\det \hat h = 1$.
3. $\operatorname{tr}(\hat h^{-1}\delta)=0$.
4. $s>0$.

No other condition is imposed. In particular:

• $\delta$ need not be symmetric. It is any real $3\times3$ matrix satisfying hypothesis 3.
• $\dot s$ is an arbitrary real number. It may be zero or negative.

The hypotheses can all be satisfied together, for example with $\hat h=I$, $\delta=0$, $s=1$ and any $\dot s$, so the statement is not vacuous.

Matrix inverse. In the code, $M^{-1}$ is Mathlib's total matrix inverse: the adjugate times the inverse of the determinant, and the zero matrix when the determinant is $0$. Here $\det\hat h=1$ and $\det(s\hat h)=s^3>0$, so both inverses that occur are genuine inverses. In particular $(s\hat h)^{-1}=s^{-1}\hat h^{-1}$.

The custom definition used. For real $3\times3$ matrices $m$ and $k$, the code defines

$$\mathrm{velocityQuad}(m,k)=\sqrt{\det m}\,\Big(\operatorname{tr}\big(m^{-1}k\,m^{-1}k\big)-\big(\operatorname{tr}(m^{-1}k)\big)^2\Big).$$

In this formula:

• $\sqrt{\cdot}$ is the real square root, which returns $0$ on negative arguments. Here $\det(s\hat h)=s^3>0$, so it is the ordinary root $s^{3/2}$.
• $m^{-1}$ is the total inverse described above.
• The definition is a plain trace expression in matrix products. It involves no symmetrization of $k$.

The assertion. Set $m=s\hat h$ (the scalar multiple) and $k=\dot s\,\hat h+s\,\delta$. The theorem claims the exact real equality

$$\sqrt{\det(s\hat h)}\,\Big(\operatorname{tr}\big((s\hat h)^{-1}k\,(s\hat h)^{-1}k\big)-\big(\operatorname{tr}((s\hat h)^{-1}k)\big)^2\Big) =-\Big(\tfrac34\sqrt{\tfrac{32}{3}}\;s^{-1/4}\,\dot s\Big)^2+\tfrac{3}{32}\Big(\sqrt{\tfrac{32}{3}}\;s^{3/4}\Big)^2\operatorname{tr}\big((\hat h^{-1}\delta)(\hat h^{-1}\delta)\big).$$

On the right-hand side:

• $s^{-1/4}$ and $s^{3/4}$ are real powers with real exponents. Since $s>0$, they are the usual positive powers $s^{-1/4}=1/s^{1/4}$ and $s^{3/4}$.
• $\sqrt{32/3}$ is the positive real square root.

Multiplying out the constants gives the same right-hand side in simpler form:

$$-6\,s^{-1/2}\,\dot s^{2}+s^{3/2}\operatorname{tr}\big((\hat h^{-1}\delta)^2\big).$$

Edge cases.

• If $\dot s=0$, the first term on the right vanishes.
• If $\delta=0$, the second term vanishes, so the claim becomes $\mathrm{velocityQuad}(s\hat h,\dot s\hat h)=-6s^{-1/2}\dot s^2$.
• No limit or derivative is involved. $\dot s$ and $\delta$ are just a number and a matrix plugged into an algebraic identity. Nothing ties $\delta$ to a path of unimodular matrices, apart from the single linear condition $\operatorname{tr}(\hat h^{-1}\delta)=0$.
• The symbol $\tau$ appears only in the docstring. It is not defined in the statement.
• The trace term $\operatorname{tr}((\hat h^{-1}\delta)^2)$ is not asserted to have any sign.