D
plain-language theorem explainer
Local alias for the spatial dimension, fixed at the natural number 3 by the T8 forcing step. Anyone citing dimension-gap identities, the eight-tick period $2^D$, generation count, or $\mathbb{F}_2^D$ constructions in this unification module uses it. The body is a one-line definition, not a proof.
Claim. The spatial dimension is the natural number $D = 3$, as forced by the T8 step of the Recognition Science forcing chain.
background
This module sits in the Unification layer and proves only arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from $D = 3$. The module doc is explicit: it does not derive the SM spectrum; it re-expresses known counts in $D$-flavored notation and kernel-checks the equalities.
Upstream, the same constant appears in Foundation.GapDerivation and Constants.AlphaDerivation as "spatial dimension, forced by T8" (resp. T9 linking). The primer landmark T8 is exactly the claim that spatial dimension equals 3. Related local siblings are the eight-tick period $2^D = 8$ and the dimension-gap polynomial evaluated at $D = 3$.
The fundamental tick $\tau_0 = 1$ and the octave of eight ticks supply the temporal cadence against which the spatial $D$ is paired, but they are not re-derived here.
proof idea
One-line definition: the natural-number literal 3 is assigned to $D$. No tactics, no lemmas, no hypotheses.
why it matters
Gives every downstream identity in FermionDOFGapBridge a single named constant for spatial dimension: eight-tick period, dimension gap at $D=3$, generations equal to $D$, and the fermionic DOF count written as a pure function of $D$. Outside the module it parameterizes $\mathbb{F}_2^D$ (cardinality $2^D$, Hamming weights, axis sums) and appears in action/geodesic scaffolding that threads the same constant.
Framework landmark: T8 of the forcing chain (Foundation.DimensionForcing), which forces $D = 3$. The module status note stresses the honest split: $D=3$ and $2^D=8$ are RS-derived upstream; the SM representation content and the $7/8$ thermal weight are imported. This definition is the local handle that keeps that split visible in the arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.