spacetime_dim

The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice to quadratic cost to Laplacian to Minkowski interval, then curved metric from defect and Einstein equations. Architecture opens with the Minkowski form on $\mathbb{R}^{1,3}$, $s^2 = -t^2 + x^2 + y^2 + z^2$, and treats Lorentzian signature, causal trichotomy, and light-cone speed limit as forced structure.

Upstream, the unified forcing chain forces spatial dimension $D = 3$ and identifies the eight-tick period as $2^D$ at that dimension (T7–T8). Temporal direction is the single tick axis; spatial directions are the three voxel axes. The present identity is the pure arithmetic glue between those forced counts and total spacetime dimension four. Sibling material in the module defines the Minkowski form, signature signs, and causal trichotomy that sit on this dimension count.

Term-mode proof discharged by norm_num: Lean reduces the closed natural-number equation $1+3=4$ by arithmetic normalization. No lemmas, no hypotheses, no case splits.

Pins the dimension clause used throughout gravity and unification. Downstream, Gravity.Connection sets spacetime dimension to 4; the master theorem’s Lorentzian-(1,3) carried proposition requires four spacetime dimensions with one timelike and three spacelike directions; Unification.SpacetimeEmergence uses it for SE-001 (spacetime has exactly four dimensions), uniqueness of the (1,3) signature, and the full SpacetimeEmergenceCert that spacetime structure is forced by the J-cost functional and forcing chain T0–T8.

In the primer landmarks this is the arithmetic face of T8 ($D=3$ spatial) plus one temporal tick, giving the familiar 4D Lorentzian stage on which continuum manifold emergence and zero-parameter gravity sit. It does not itself force $D=3$; it only records the sum once that forcing is in place.