The spatial slice of the single-time world is a spacelike data surface
ProvedTegmark.spacelike_sliceThe positive half of the data-surface argument (pages L73-L74): hyperbolic equations allow well-posed initial-value problems, and specifying initial data on the spatial slice determines the solution in the volumes bounded by the cones, so that a localized observer can make predictions about its future. The theorem constructs the data surface for every single-time world: in a world with n space dimensions and exactly one time dimension, the spatial slice — the kernel of the time-coordinate projection — is a spacelike hyperplane; the quadratic form on it is the sum of the squares of the space coordinates, positive on every nonzero vector.
Formalization Note The witness is the time-coordinate projection; the statement is the existence half of the predictability requirement's data-surface clause, for every number of space dimensions.
import Mathlib import Definitions.Def_Tegmark_sig import Definitions.Def_Tegmark_phys import Definitions.Def_Tegmark_ensemble
namespace Tegmark /-! # The spacelike slice of the single-time world With exactly one time dimension, the spatial slice of an "(n, 1)" world, the kernel of the time-coordinate projection, is a spacelike hyperplane: the quadratic form is the sum of squares of the space coordinates on it, positive on every nonzero vector. Single-time worlds therefore possess the data surfaces on which observers record initial conditions (Tegmark 1997, pp. L73-L74). -/ /-- In a world with "n" space dimensions and exactly one time dimension there is a spacelike hyperplane (Tegmark 1997, pp. L73-L74): the spatial slice, on which the form is positive definite. -/ theorem spacelike_slice (n : ℕ) : HasSpacelikeHyperplane n 1 := by sorry end Tegmark
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every natural number n, there exists a linear functional from the coordinate space of the world with n space dimensions and one time dimension to the real numbers which is nonzero and whose kernel is spacelike: on every nonzero vector of the kernel, the quadratic form — the sum of the squares of the space coordinates minus the square of the single time coordinate — is positive. The existential quantifies over all linear functionals; no hypotheses appear.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.