pith. machine review for the scientific record. sign in
def definition def or abbrev high

Spacetime

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  47def Spacetime : Manifold := { dim := 4 }

proof body

Definition body.

  48
  49/-- Coordinate indices for spacetime. -/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.