spacetime_dim
plain-language theorem explainer
Total spacetime dimension equals the sum of one temporal dimension (octave advance) and three spatial dimensions (T8). Researchers assembling the emergent 4D Lorentzian structure from J-cost minimization cite this when combining the forced counts. It is a direct arithmetic sum of the two upstream dimension definitions.
Claim. Spacetime dimension is defined as $d = d_t + d_s$, where $d_t = 1$ is the single octave advance and $d_s = 3$ is the spatial count forced by T8.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure from the J-cost functional and the T0-T8 forcing chain. Temporal dimension counts the unique cost-reducing direction of the 8-tick recognition operator. Spatial dimension is fixed at three by T8. Upstream results supply the separate definitions: temporal_dim equals 1 and spatial_dim equals D_physical.
proof idea
One-line definition that adds the values of temporal_dim and spatial_dim.
why it matters
This definition supplies the input to spacetime_dim_eq_four (which proves equality to 4) and to SpacetimeEmergenceCert (which verifies the full forced Lorentzian structure). It realizes the dimension-count step in the module derivation chain: RCL to J-uniqueness (T5) to 8-tick octave (T7) plus D=3 (T8) to total dimension 4. It is referenced by signature_unique and by the Gravity.Connection spacetime_dim alias.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.