Spacetime
plain-language theorem explainer
Spacetime is defined as the four-dimensional manifold in the Recognition Science geometry scaffold. Researchers working on QFT cutoffs or entanglement entropy would reference this placeholder to type-check spacetime structures. The definition is a direct one-line assignment of dimension four to the Manifold record.
Claim. Let $M$ be the manifold structure with dimension field $d : ℕ$. Spacetime is the instance of $M$ with $d = 4$.
background
The Manifold structure is a record carrying a single field dim : ℕ together with a Repr instance. This supplies the minimal typed carrier for points and coordinate charts in the module. The module itself is explicitly marked as a scaffold that is not part of the verified certificate chain; its purpose is only to let downstream modules type-check. Upstream, the dimension value 4 is independent of the spatial dimension D supplied by TauStepDerivation.dim and of the meta-realization structure for in UniversalForcingSelfReference.for.
proof idea
One-line definition that constructs the Manifold record with its dim field set to the literal 4.
why it matters
This definition supplies the typed spacetime manifold used by downstream structures such as RealityCertificate, UVCutoffFalsifier, and IsSmoothRecognitionGeometry. It fills the placeholder role in the Relativity geometry module, enabling type-checking for recognition geometry charts and dimension status. As a scaffold it touches the open question of full differential geometry formalization in the verified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.