rsSpacetimeDim_lorentzian
The spacetime dimension derived from the recognition manifold is fixed at four. Researchers deriving Lorentzian geometry from recognition principles cite this when confirming the 3+1 structure. The proof is a direct one-line reference to the decidable equality that computes the dimension as spatial dimension plus one.
claimThe spacetime dimension in the Recognition Science framework equals four: $D+1=4$, where $D$ is the spatial dimension of the recognition manifold.
background
The module derives five canonical differential geometric structures from the recognition manifold, a smooth 3-manifold with spatial dimension $D=3$. The RS metric is pseudo-Riemannian, yielding spacetime of dimension $D+1=4$. The definition of spacetime dimension is the natural number obtained by adding one to the spatial dimension. An upstream result establishes equality to four via a decision procedure.
proof idea
The proof is a one-line wrapper that directly invokes the equality theorem proved by the decide tactic.
why it matters in Recognition Science
This result confirms the 3+1 Lorentzian spacetime dimension required by the Recognition Science framework at T8. It supports the pseudo-Riemannian structure and the count of five differential structures for $D=3$. It closes the dimension count in the module.
scope and limits
- Does not derive the spatial dimension independently.
- Does not specify the metric signature or curvature.
- Does not connect to physical constants or mass formulas.
formal statement (Lean)
32theorem rsSpacetimeDim_lorentzian : rsSpacetimeDim = 4 := rsSpacetimeDim_eq_4
proof body
33