rsSpacetimeDim_eq_4
plain-language theorem explainer
The declaration establishes that the spacetime dimension computed from the recognition manifold is exactly four. Researchers deriving differential geometry from Recognition Science would cite it when confirming the four-dimensional structure of spacetime. The proof is a direct decision procedure evaluating the definition that adds one to the three-dimensional manifold dimension.
Claim. The spacetime dimension derived from the three-dimensional recognition manifold equals four.
background
In this module the recognition manifold is a smooth 3-manifold. The spacetime dimension is obtained by adding one to the manifold dimension, producing the four-dimensional structure required for the pseudo-Riemannian RS metric. The upstream definition states that the spacetime dimension equals the manifold dimension plus one.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the definition of the spacetime dimension as the manifold dimension plus one, confirming the value four.
why it matters
This supplies the spacetime dimension value required by the DiffGeoCert structure that records five geometric structures and the four-dimensional spacetime. It implements the module statement that the RS metric is pseudo-Riemannian with dimension D+1 equal to four, consistent with the framework derivation of four-dimensional spacetime from three spatial dimensions. The result is also used directly by the Lorentzian variant statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.