rsSpacetimeDim
plain-language theorem explainer
The definition sets spacetime dimension to spatial dimension plus one. Recognition Science researchers cite it when fixing the 3+1 Lorentzian structure from the underlying 3-manifold. It is a direct one-line arithmetic extension of the rsDimension constant.
Claim. The spacetime dimension is defined by $D + 1$, where $D = 3$ is the dimension of the recognition manifold.
background
The module Differential Geometry from RS takes the recognition manifold to be a smooth 3-manifold. It establishes five canonical differential geometric structures on this manifold, with configDim D = 5. The RS metric is pseudo-Riemannian, so spacetime arises as the 4-dimensional extension D + 1, which equals 3 + 1 and carries the Lorentzian signature.
proof idea
This is a one-line definition that computes rsSpacetimeDim directly as rsDimension plus one, where the upstream rsDimension definitions in the same module, LinearAlgebraFromRS, and SuperstringTheoryFromRS each fix the value at 3.
why it matters
The definition supplies the spacetime dimension required by DiffGeoCert to certify both the five structures and the equality to 4. It implements the extension from spatial D = 3 (T8 in the forcing chain) to the full 4-dimensional Lorentzian spacetime demanded by the RS metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.