Dimension
plain-language theorem explainer
Spatial dimension is introduced as a plain natural-number parameter. Anyone writing T7/T8 substrate axioms, cube-graph cellular completions, or configuration-space counts cites this alias. The body is a one-line type synonym for ℕ, with no proof obligations.
Claim. The spatial dimension parameter is a natural number $D \in \mathbb{N}$.
background
The module T7.5 Substrate Axioms records the structural inputs for the T7/T8 dimension route: predicate-level commitments (cellular completions, tame cube-graph embeddings, retractions) without claiming a full Mathlib smooth-topology chain.
In Recognition Science the spatial dimension is forced to three by the linking requirement (T8 / T9). Upstream constants already fix $D := 3$ and the eight-tick period $2^D = 8$. A separate dimensional-signature structure tracks physical $[L,T,M]$ exponents; the present alias is the bare count of spatial axes, not that signature.
Sibling predicates (cellular completion of the cube graph in dimension $D$, one-acyclic substrate, loop entanglement) all take this parameter.
proof idea
Pure definitional abbreviation: Dimension is identified with the type of natural numbers. No tactics, no lemmas, no hypotheses.
why it matters
This alias is the common type for every T7.5 substrate clause and for the curvature-space derivation stack. Downstream results that consume it include spatial_dims_eq_3 (spatial dimensions forced to 3), eight_tick_forces_temporal ($2^D = 8$), config_space_is_5D (3 spatial + 1 temporal + 1 dual-balance), and the complete curvature-term derivation feeding $\alpha$. Physical dimension tracking (dim_c, DimensionedQuantity) also re-exports the name. It sits at the T7–T8 landmark: eight-tick octave forces $D = 3$ spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.