Spacetime
plain-language theorem explainer
Spacetime is defined as the four-dimensional manifold in the Recognition geometry scaffolding. Workers on QFT cutoffs and entanglement entropy would cite it to fix total dimension at four when typing points and covectors. The definition is a direct record construction that supplies the dimension field of the Manifold structure.
Claim. Spacetime is the smooth manifold $M$ satisfying $dim(M) = 4$.
background
The module supplies placeholder manifold types for the Relativity geometry layer. Manifold is the structure carrying a natural-number dimension together with coordinate charts. Upstream, the spatial dimension is fixed at three by the TauStepDerivation.dim definition, which pulls D from the eight-tick octave of the forcing chain; spacetime therefore augments that value by one time coordinate.
proof idea
One-line definition that constructs the Manifold record with dimension field set to four.
why it matters
The definition supplies the four-dimensional carrier required by RealityCertificate, UVCutoffFalsifier, and IsSmoothRecognitionGeometry. It implements the 3+1 split implied by T8 while remaining outside the verified certificate chain, leaving open the question of lifting the placeholder into the core Recognition geometry formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.