pith. machine review for the scientific record. sign in
def definition def or abbrev high

spacetime_dim

show as:
view Lean formalization →

Spacetime dimension is defined as the sum of one temporal dimension and three spatial dimensions. Researchers deriving Lorentzian geometry from J-cost minimization would cite this when assembling the total count from the forcing chain. The definition is a direct arithmetic sum of the two component constants established upstream.

claimThe spacetime dimension is $d = d_t + d_s$, where $d_t = 1$ is the temporal dimension corresponding to the octave advance and $d_s = 3$ is the spatial dimension forced by the T8 step.

background

The Spacetime Emergence module derives the full structure of 4D Lorentzian spacetime from the J-cost functional and the T0-T8 forcing chain rather than postulating a background manifold. The module states that spacetime 'is not a background postulate. It is a theorem of cost minimization' and that 'Dimension = 4: 1 temporal (octave) + 3 spatial (D = 3 from T8)'. Temporal dimension is fixed at 1 to match the 8-tick recognition operator period. Spatial dimension is fixed at D_physical = 3 from the T8 step in the phi-ladder.

proof idea

This is a one-line definition that adds the values of temporal_dim and spatial_dim.

why it matters in Recognition Science

This definition supplies the total dimension count to the SpacetimeEmergenceCert structure and the signature_unique theorem proving that the (1,3) signature is the unique RS-compatible one. It realizes the SE-001 claim by combining the T7 octave (temporal) with the T8 spatial count, supporting the module's derivation of the Lorentzian metric η = diag(−1, +1, +1, +1) with zero free parameters.

scope and limits

formal statement (Lean)

  68def spacetime_dim : ℕ := temporal_dim + spatial_dim

proof body

Definition body.

  69
  70/-- **SE-001: Spacetime has exactly 4 dimensions.** -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.