spacetime_dim
plain-language theorem explainer
The spacetime dimension is defined as the sum of the temporal dimension (one octave advance) and the spatial dimension (three axes forced by T8). Researchers deriving Lorentzian geometry from the J-cost functional cite this when assembling the four-dimensional structure required by the forcing chain. It is a direct arithmetic definition that combines the two component counts already established upstream.
Claim. Define the total spacetime dimension by $d := d_t + d_s$, where the temporal dimension $d_t$ equals 1 (the octave advance) and the spatial dimension $d_s$ equals 3 (forced by T8).
background
The Spacetime Emergence module derives the full structure of 4D Lorentzian spacetime from the J-cost functional and the T0–T8 forcing chain. Temporal dimension is defined as exactly 1, the unique cost-reducing direction under the 8-tick recognition operator. Spatial dimension is defined as D_physical = 3, the count forced by T8 in the chain (see upstream spatial_dim and temporal_dim).
proof idea
This is a definition that directly adds the values of temporal_dim and spatial_dim in the natural numbers. No lemmas or tactics are applied; the body is the arithmetic sum.
why it matters
This supplies the total dimension used by spacetime_dim_eq_four (which proves equality to 4), signature_unique (which confirms the (1,3) signature is unique), and the SpacetimeEmergenceCert structure. It realizes the module's central claim that 1 temporal octave plus D = 3 spatial dimensions yields four-dimensional spacetime forced by RCL and T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.