rsSpacetimeDim_lorentzian
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.