DeWitt supermetric is positive on traceless momenta

Proved

WheelerDeWittSuperspace.superQuad_pos_of_traceless

by Mazecto · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

general-relativitymathematical-physicsquantum-gravity

Let $h$ be a positive-definite $3\times3$ matrix and $p\neq0$ a symmetric matrix with $\operatorname{tr}(hp)=0$ . Then

G_{abcd}(h)\,p^{ab}p^{cd}>0,\qquad G_{abcd}=\frac{h_{ac}h_{bd}+h_{ad}h_{bc}-h_{ab}h_{cd}}{2\sqrt{\det h}}.

This is the positive five-dimensional part of the Lorentzian signature of the supermetric.

Preamble

import Definitions.Def_WheelerDeWittSuperspace

set_option autoImplicit false

open Matrix

Formal statement

namespace WheelerDeWittSuperspace

/-- Milestone 1 (Lorentzian signature, positive part): the supermetric is positive on
nonzero symmetric momenta that are traceless with respect to `h`. -/
theorem superQuad_pos_of_traceless (m p : Matrix (Fin 3) (Fin 3) ℝ) (hm : m.PosDef)
    (hp : pᵀ = p) (hp0 : p ≠ 0) (htr : (m * p).trace = 0) :
    0 < superQuad m p := by sorry

end WheelerDeWittSuperspace

Source

B. S. DeWitt, Quantum Theory of Gravity I. The Canonical Theory, Phys. Rev. 160 (1967) 1113-1148, https://doi.org/10.1103/PhysRev.160.1113, Section 5; C. Kiefer, Quantum Geometrodynamics: whence, whither?, Gen. Relativ. Gravit. 41 (2009) 877-901, https://arxiv.org/abs/0812.0295, eq. (5)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Theorem superQuad_pos_of_traceless. Let $m = (m_{ab})$ and $p = (p^{ab})$ be arbitrary real $3\times 3$ matrices, with indices $a,b \in \{0,1,2\}$ . Assume:

$m$ is positive definite in Mathlib's sense. This means $m$ is symmetric ( $m^{\mathsf T} = m$ ) and $x^{\mathsf T} m\, x > 0$ for every nonzero $x \in \mathbb{R}^3$ . In particular $\det m > 0$ .
$p$ is symmetric: $p^{\mathsf T} = p$ .
$p \neq 0$ (not the zero matrix).
$\operatorname{tr}(m\,p) = \sum_{a,b} m_{ab}\, p^{ba} = 0$ . The trace condition pairs $p$ with the matrix $m$ itself, not with $m^{-1}$ .

The conclusion is the strict inequality

0 < \mathcal{G}_m(p),

where $\mathcal{G}_m(p)$ (the definition superQuad) is the full quadruple sum

\mathcal{G}_m(p) = \sum_{a=0}^{2}\sum_{b=0}^{2}\sum_{c=0}^{2}\sum_{d=0}^{2} G_{abcd}(m)\, p^{ab}\, p^{cd},

and the coefficients (the definition deWitt) are

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

where $V$ (the definition volume) is the real square root. Under hypothesis 1, $\det m > 0$ . So $V(m) > 0$ , and the truncated square root and division by zero never produce junk values. The coefficients are built from $m$ with lower indices directly; the inverse $m^{-1}$ does not appear.

Unfolding the sum with $m$ and $p$ symmetric, the claim reads

\frac{2\operatorname{tr}(m p m p) - \big(\operatorname{tr}(m p)\big)^2}{2\sqrt{\det m}} > 0,

which under hypothesis 4 becomes $\operatorname{tr}(m p m p) > 0$ .

Edge cases. There are no implicit binders, type parameters or typeclass assumptions: the dimension is fixed at $3$ and the scalars are real. The hypotheses can all hold together, so the statement is not vacuous. For example, $m = I$ and $p = \operatorname{diag}(1,-1,0)$ satisfy all four. The statement says nothing about matrices $p$ that are not symmetric or that have $\operatorname{tr}(mp) \neq 0$ , or about matrices $m$ that are not positive definite.

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph