T8_Dimension_TripleRoute_Bridge
plain-language theorem explainer
Packages the T8 spatial-dimension claim as five Prop fields: linking (Alexander duality), eight-tick (2^D = 8), gap-sync upper bound (2^D divides the sync period), Clifford spinor plus eight-tick, and uniqueness from full RS-compatibility. Anyone citing the complete forcing chain or D = 3 will reference this bridge. It is a pure interface structure; the inhabitant is supplied elsewhere.
Claim. A proposition recording five forcing statements for spatial dimension $D$: (i) nontrivial circle linking in $S^D$ implies $D=3$; (ii) $2^D=8$ implies $D=3$; (iii) $2^D\mid 360$ implies $D\le 3$; (iv) an RS spinor structure together with the eight-tick equation implies $D=3$; (v) full RS-compatibility of $D$ implies $D=3$.
background
In the Unified Forcing Chain, T0–T8 are claimed as inevitabilities from the Recognition Composition Law plus normalization and calibration. T7 fixes the eight-tick octave (period $2^3$); T8 closes the loop by forcing spatial dimension $D=3$.
DimensionForcing.Dimension is the discrete spatial dimension parameter used in that module (not the LTM dimensional signature). The eight-tick constant is the fundamental evolution period of eight ticks. RS-compatibility of a candidate $D$ is the conjunction of linking support, eight-tick matching, and gap-sync divisibility; the Clifford bridge supplies the spinor characterization via Bott periodicity ($\mathrm{Cl}_{n+8}\cong\mathrm{Cl}_n\otimes\mathrm{Cl}_8$).
The module’s chain diagram lists T8 as “$D=3$ ← linking + gap-45 sync,” with the eight-tick route as the independent $2^D=8$ reduction already tied to T7.
proof idea
No proof body: this is a structure ... : Prop interface. Each field is a named universal statement over candidate dimensions. Downstream, t8_triple_route_bridge_holds builds an inhabitant from T8_Dimension_Forced by assigning linking_route to the forced linking lemma, eight_tick_route to DimensionForcing.eight_tick_forces_D3, discharging the gap-sync upper bound by a short divisibility argument, and wiring the spinor and three-route uniqueness fields from the same forced package. The structure itself only records the shape of those obligations.
why it matters
T8 is the last rung of the forcing chain: once $D=3$ is forced, the eight-tick octave, hypercube vertex count $2^D$, and RS-native constants that depend on spatial dimension sit on a unique value. The primer landmark is exactly this step (T8: $D=3$).
CompleteForcingChain includes the T8 layer among “all of T0–T8 forced from the cost foundation.” The companion theorem t8_triple_route_bridge_holds is the witness that every route holds unconditionally and that their conjunction uniquely determines $D=3$. The design point is redundancy: linking is primary, eight-tick is an independent cross-check, gap-sync is a consistency bound, and the spinor route ties Clifford structure to the same conclusion so no single topological or arithmetic accident carries the claim alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.