dimension_unique_via_realization
plain-language theorem explainer
Any spatial dimension satisfying the full RS-compatibility package (nontrivial linking, eight-tick sync, gap-45 divisibility, and the T7.5 substrate/loop conditions) equals 3. Cited by anyone assembling the realization-route form of T8. Proof is a one-line extraction of the linking field, discharged by the Alexander-duality forcing lemma.
Claim. Let $D\in\mathbb{N}$ be a spatial dimension. If $D$ is RS-compatible, meaning it supports nontrivial linking, realizes the eight-tick period as $2^D$, divides the gap-45 synchronization period, and carries the T7.5 package (cellular completion, one-acyclic substrate, loop entanglement, and compatibility with the realized cycle), then $D=3$.
background
The DimensionForcing module establishes that spatial dimension $D=3$ is forced inside Recognition Science, not chosen. The classical topological route is the linking argument: only in three dimensions do closed curves support stable nontrivial linking (knots and links with nontrivial fundamental group of the complement). In $D\le 2$ everything unlinks or cannot link; in $D\ge 4$ codimension lets curves pass freely. Ledger conservation needs that stable linking, so $D=3$.
RSCompatibleDimension packages that linking demand together with the eight-tick identity $2^D=8$, gap-45 sync divisibility, and the T7.5 substrate conditions (cellular completion, one-acyclic substrate, loop entanglement, compatibility with the realized cycle). The numerical constant $D$ used elsewhere in the constants layer is already set to 3 by the same linking principle.
Upstream, the decisive lemma is the Alexander-duality statement that nontrivial linking exists if and only if $D=3$ (Hatcher Thm 3.44 style). The present theorem simply routes the realization package through that lemma.
proof idea
Term-mode one-liner. Introduce the RS-compatibility hypothesis $h$, project out its linking field $h.linking$ (the SupportsNontrivialLinking component), and apply the existing lemma linking_requires_D3 to that field. No other fields of the package are consulted; eight-tick, gap-sync, and the T7.5 substrate axioms ride along only as part of the hypothesis type.
why it matters
This is the realization-route discharge of T8 in the forcing chain (T0–T8). Downstream it is consumed by t8_via_realization_bridge_holds in UnifiedForcingChain, which builds the T8-via-realization bridge from T7 plus the T7.5 cellular-completion and one-acyclic bridges. The module-level dimension-forcing theorem records the same conclusion: once linking is required, Alexander duality pins $D=3$, and the eight-tick period $2^D=8$ together with $\mathrm{lcm}(8,45)=360$ become consequences rather than premises. The refined paper route named here keeps the full T7.5 substrate/loop package inside the hypothesis while still finishing on the classical linking theorem, so the numerical uniqueness of dimension is not a free parameter anywhere in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.