Positive spatial metric volume density

Proved

WheelerDeWitt.volumeDensity_pos

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

canonical-quantizationmathematical-physicsquantum-gravity

For every supplied spatial geometry, configuration and spatial point, the square root of the positive metric determinant is strictly positive.

Preamble

import Definitions.Def_wdw_canonical_operators
set_option autoImplicit false

Formal statement

namespace WheelerDeWitt

theorem volumeDensity_pos {C X : Type*} (g : Geometry C X) (q : C) (x : X) :
    0 < volumeDensity g q x := by
  sorry

end WheelerDeWitt

Source

Claus Kiefer, Quantum Geometrodynamics: whence, whither?, Gen. Relativ. Gravit. 41 (2009), 877–901, https://arxiv.org/abs/0812.0295, Sections 2.2 and 2.4, equations (3)–(8). Formal algebraic derivation with supplied geometry and complex-linear derivative interface; no analytic realization asserted.

Read-back

What the Lean code literally says, in plain math · Codex (inherited session model)

For arbitrary types $C,X$ , every family $h(q,x)$ of real positive-definite $3×3$ matrices with separately supplied proofs that $\det h(q,x)>0$ at all pairs and an arbitrary real-valued function $R(q,x)$ , and every $q∈C,x∈X$ , the assertion is $0<\sqrt{\det h(q,x)}$ , which is precisely strict positivity of the defined volume density. No nonemptiness of $C$ or $X$ is assumed; the quantified assertion has no instances if either type is empty. No regularity or connection between $R$ and the matrix family is assumed.

View graph