Spacetime closedness theorem for homogeneous Lorentzian foliations

Abstract

Motivated by the geometric interpretation of spatially homogeneous cosmological models, we formulate a spacetime closedness theorem directly at the Lorentzian level. A classical space-form classification theorem organizes homogeneous and isotropic spatial geometries, but by itself it does not yield a Lorentzian statement about the ambient spacetime. The main technical step is to derive finite slice-volume from genuinely Lorentzian control hypotheses on the foliation. This is achieved in a strong version, for maximally regular globally hyperbolic $(n+1)$--spacetimes with a finite-time Big Bang and homogeneous complete spacelike slices, and in a weaker version in which maximal regularity is replaced by time-integrability of the accumulated expansion rate. In both cases, the argument separates an analytic step, deriving finite slice-volume from the Big Bang and temporal control, from a geometric step, upgrading finite volume to compactness by homogeneity and completeness. The theorem is stated in arbitrary spacetime dimension and is accompanied by a Lean~4 formalization of the strong and weak abstract statements.

arXiv comment11 pages

References in corpus (7)

• On smooth Cauchy hypersurfaces and Geroch's splitting theorem
• Smoothness of time functions and the metric splitting of globally hyperbolic spacetimes
• Spacelike hypersurfaces of constant higher order mean curvature in generalized Robertson-Walker spacetimes
• Null distance and convergence of Lorentzian length spaces
• Characterization of some causality conditions through the continuity of the Lorentzian distance
• Time functions on Lorentzian length spaces
• A Canonical Complex Structure and the Bosonic Signature Operator for Scalar Fields in Globally Hyperbolic Spacetimes