spacetime_dim
plain-language theorem explainer
Spacetime dimension is fixed at four to support local coordinate calculations of the Levi-Civita connection. Researchers deriving general relativity from the Recognition Science forcing chain cite this definition when establishing the 4D patch for metric and Christoffel computations. It inherits the value directly from the upstream spacetime emergence result that sums temporal and spatial dimensions. The implementation is a one-line constant assignment with no further computation.
Claim. The spacetime dimension is defined as $4$.
background
The Gravity.Connection module works in a coordinate patch where the metric is a smooth matrix-valued function on R^4, avoiding the Mathlib abstract manifold gap. It introduces the metric tensor as a symmetric nondegenerate bilinear form g_mu nu and the Christoffel symbols via the standard formula Gamma^rho_mu nu = (1/2) g^rho sigma (partial_mu g_nu sigma + partial_nu g_mu sigma - partial_sigma g_mu nu). The local setting is chosen so that all GR computations remain rigorous in coordinates. This definition of spacetime dimension aligns with the upstream result from SpacetimeEmergence that spacetime_dim equals temporal_dim plus spatial_dim, which is shown to equal four by the eight-tick octave and D=3 spatial dimensions.
proof idea
The declaration is a direct definition that assigns the constant value 4. It functions as a one-line wrapper that ensures the gravity module uses the same dimension as the upstream spacetime emergence definition.
why it matters
This definition supports the spacetime emergence certificate that verifies 4D Lorentzian spacetime is forced by the J-cost functional and the RS forcing chain T0-T8. It is referenced by the uniqueness theorem for the (1,3) signature and by spacetime_dim_eq_four. The result connects to the T8 step that forces D=3 spatial dimensions, yielding total dimension 4, and enables subsequent connection computations in the gravity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.