t8_dimension_unique_from_linking
plain-language theorem explainer
Whenever a spatial dimension admits nontrivial linking of closed curves, that dimension must be three. Spine auditors cite this to record that the uniqueness half of T8 discharges from the linking predicate alone, with no eight-tick, gap-sync, or substrate hypotheses. The proof is a one-line term applying the primary Alexander-duality forcing theorem.
Claim. Let $D$ be a spatial dimension. If $D$ supports nontrivial linking of closed curves (equivalently, $S^D$ admits disjoint embedded circles with nonzero linking number), then $D = 3$.
background
This module is the July 2026 honesty audit of the T6–T8 forcing spine. It tags each claim as THEOREM, FORCED-CONDITIONAL, MODEL/ENCODING, or OPEN, and does not upgrade any tier; it only records what the repository already proves about its own gaps.
Spatial dimension here is a natural number. The linking predicate is topological, not combinatorial: a dimension supports nontrivial linking when the sphere $S^D$ admits disjoint $S^1$-embeddings with nonzero linking number. By Alexander duality this is equivalent to $\tilde H_1(S^D \setminus S^1) \cong \tilde H^{D-2}(S^1) \cong \mathbb{Z}$, which holds if and only if $D = 3$. The predicate deliberately replaces an older circular definition that equated dimension with the eight-tick count $2^D = 8$.
The upstream primary theorem states: "Linking requires $D = 3$. Proof: Alexander duality — no reference to 8-tick or gap-45." Constants packages elsewhere fix the forced value as the literal $D := 3$.
proof idea
One-line term proof. Apply the primary T8 theorem that nontrivial linking forces dimension three (itself the left-to-right direction of the Alexander-duality circle-linking equivalence) to the given dimension and linking hypothesis. No further tactics, no appeal to eight-tick period, gap synchronization, or substrate axioms.
why it matters
This is the audit-facing packaging of T8 in the forcing chain (T0–T8): spatial dimension three is forced by linking alone. The doc-comment stresses that dimension uniqueness discharges from the linking field only; eight-tick, gap-sync, and substrate fields are unused. Downstream it is bundled into the T6–T8 spine audit certificate structure and the checked certificate theorem that assembles the July 2026 honesty report.
The same doc-comment flags an honesty gap: the genuine $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ certificate is proved separately and remains OPEN as a premise of this discharge (not machine-checked at this call site). Sibling audit entries record that same-sector linking arithmetic still permits every odd $D \ge 3$, so the loop-loop specialization is an extra modeling choice beyond bare linking. Together these entries keep T8 honest rather than overclaimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.