without
plain-language theorem explainer
Spatial dimension three is forced in the Recognition chain: nontrivial linking, the eight-tick period, and a unique RS-compatible dimension all pin D = 3. Anyone citing T8 in the unified forcing chain, or deriving tick-scaled constants and shell chemistry from D = 3, depends on this package. The local bridge note records that the T7 eight-tick surface still admits predicate-level cellular completions in every dimension, without revising the T8 statement or its witness.
Claim. The T8 package asserts: (i) if dimension $D$ supports nontrivial linking then $D = 3$; (ii) if the eight-tick period constructed from $D$ equals the canonical eight-tick then $D = 3$; (iii) there is a unique $D$ that is RS-compatible. Separately, the T7 eight-tick surface admits predicate-level cellular completions in every dimension (T7.5a bridge), recorded so that this extension does not alter the T8 statement or its proof witness.
background
Module UnifiedForcingChain packages the complete inevitability chain from the cost foundation (Recognition Composition Law, normalization, calibration) through T-1 to T8. T7 forces the eight-tick octave (period $2^3$); T8 forces spatial dimension $D = 3$ rather than leaving it free.
The T8 structure is a proposition with three fields: linking forces $D = 3$, eight-tick forces $D = 3$, and uniqueness of an RS-compatible dimension. Upstream, the bridge module already supplies a witness t8_holds by assembling linking_requires_D3, eight_tick_forces_D3, and dimension_forced from dimension-forcing lemmas.
The fundamental tick $\tau_0 = 1$ is the RS-native time quantum; one octave is eight ticks. The T7.5a bridge sits between the eight-tick surface and cellular/predicate completions, and is written so the T8 API stays fixed.
proof idea
No local proof body is attached to this declaration in the extract (zero body lines). Substantive content lives in the referenced T8 structure and the upstream witness: t8_holds is a structure value whose three fields are exactly the dimension-forcing lemmas linking_requires_D3, eight_tick_forces_D3, and dimension_forced. The present item is bookkeeping around that package: a T7.5a bridge claim (eight-tick surface admits predicate-level cellular completions in every dimension) recorded without modifying T8_Dimension_Forced or t8_holds. Treat it as an interface/bridge note, not a fresh tactic script.
why it matters
T8 is the terminal step of the forcing chain in the primer: $D = 3$ from linking plus gap-45 sync, with T7's eight-tick as $2^D$. Downstream uses fan out widely (on the order of forty edges): positivity of $\tau_0$, $\alpha$ seam numerators at $D = 3$, exponential-form uniqueness for $\alpha$, and chemistry proxies (noble-gas EN/EA zeros, ionization sawtooth reset, shell comparisons). Astrophysics habitability bands on the $\varphi$-ladder also sit on the same constant stack. Keeping T7.5a cellular completions from rewriting T8 protects that stable API while the chain is extended. Open surface: cellular completions in every dimension must stay compatible with the uniqueness claim that only $D = 3$ is RS-compatible for physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.