T8_Dimension_Forced
plain-language theorem explainer
T8 packages the claim that spatial dimension is forced to three: nontrivial linking, the identity 2^D = 8 for the eight-tick period, and uniqueness of an RS-compatible dimension all pin D = 3. Anyone citing the complete forcing chain or the T8-to-T7 bridge uses this interface. It is a Prop-structure that collects three DimensionForcing statements; the fields are discharged elsewhere, not proved in the structure body.
Claim. The T8 interface asserts three claims about spatial dimension $D$: (i) every $D$ that supports nontrivial linking equals $3$; (ii) if the eight-tick period built from $D$ equals $8$ (i.e. $2^D = 8$), then $D = 3$; (iii) there exists a unique $D$ that is RS-compatible (linking plus the eight-tick and gap-45 constraints).
background
In the Unified Forcing Chain, every landmark from the absolute floor through T8 is presented as forced from the cost foundation (Recognition Composition Law, normalization, calibration). T8 is the terminal spatial step: dimension is not a free parameter.
Upstream, DimensionForcing defines the eight-tick period as the constant $8$, and the period derived from a candidate dimension as $2^D$. The theorem eight_tick_forces_D3 states that $2^D = 8$ implies $D = 3$, via a pure power-of-two argument. Nontrivial linking (ledger conservation that needs genuine linking of cycles) and RS-compatibility bundle the same $D = 3$ conclusion with gap-45 synchronization (the rung-45 barrier, equal to $D^2(D+2)$ at $D = 3$).
Constants modules already fix the RS-native tick $\tau_0 = 1$ and set the derived spatial dimension constant to $3$, with $2^D$ vertices on the hypercube. T8 is the Prop-level certificate that those choices are forced rather than stipulated.
proof idea
No proof body: this is a structure-as-Prop with three fields. It records the T8 interface only.
Discharge happens at the bridge theorem that builds an inhabitant by assigning linking_forces_D3 to the DimensionForcing linking theorem, eight_tick_forces_D3 to the power-of-two theorem (unfold $2^D = 8$, apply the unique-$D$ lemma for powers of two), and unique_dimension to the DimensionForcing uniqueness theorem for RS-compatible dimension. Downstream bridges then project these fields (e.g. linking implies $D = 3$) without re-proving them.
why it matters
T8 is the chain landmark "D = 3 spatial dimensions" in the primer and the module's complete inevitability list (after T7 eight-tick as $2^D$ with $D = 3$). The doc-comment states the three forcing routes: nontrivial linking for ledger conservation, $2^D = 8$ eight-tick sync, and gap-45 synchronization.
Parents: the T−1-to-T8 complete chain structure, the bridge that derives T7 from a T8 witness (eight-tick as $2^3$ once $D = 3$), the public-spine substrate certificate (honest replacement for a mere Nonempty T8 wrapper), and the in-module CompleteForcingChain. Without this interface the chain cannot close spatial dimension or hand a typed $D = 3$ fact to eight-tick and constants (including $\alpha$ machinery that imports $D$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.