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

spatial_dim

show as:
view Lean formalization →

Defines the spatial dimension count as exactly 3, the value forced by the T8 step of the Recognition Science forcing chain. Researchers deriving Lorentzian geometry from J-cost minimization would reference this when establishing the (1,3) metric signature. The definition is a direct alias for the upstream D_physical constant.

claimThe number of spatial dimensions is $D=3$, as required by the T8 step of the Recognition Science forcing chain.

background

Recognition Science derives the full structure of 4D Lorentzian spacetime from the J-cost functional and the T0–T8 forcing chain. The module shows that the metric signature (−,+,+,+), light cones, and arrow of time arise as theorems of cost minimization rather than background postulates. Spatial curvature is positive definite because J''(1)=1, while the temporal direction is the unique cost-reducing axis set by the 8-tick recognition operator.

proof idea

One-line definition that aliases the upstream D_physical value.

why it matters in Recognition Science

This supplies the spatial count required by the downstream theorems that establish the unique Lorentzian signature (1,3). It implements the T8 step of the forcing chain and feeds directly into lorentzian_signature, signature_unique, spacetime_dim, and SpacetimeEmergenceCert. The parent results close the derivation of η = diag(−1,+1,+1,+1) with zero free parameters.

scope and limits

formal statement (Lean)

  65def spatial_dim : ℕ := D_physical

proof body

Definition body.

  66
  67/-- Total spacetime dimension: temporal + spatial. -/

used by (8)

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

depends on (1)

Lean names referenced from this declaration's body.