dimension_three_from_linking_requirement
plain-language theorem explainer
Assuming uniqueness of three-dimensional linking, any natural-number dimension that admits a strictly positive Hopf linking penalty equals three. Cite this on the T8 / linking branch of dimension forcing in Recognition Science. The argument is a one-line right-to-left application of the uniqueness hypothesis at the given dimension.
Claim. Assume that $D=3$ is the unique natural number for which a positive Hopf linking penalty exists (i.e., $D=3$ iff there is a real penalty $>0$ equal to the Hopf linking penalty). Then for every $D\in\mathbb{N}$, if such a positive penalty equal to the Hopf linking penalty exists, one has $D=3$.
background
The module Verification.Dimension is built to force spatial dimension three. Its main path uses RSCounting plus 45-gap synchronization and an arithmetic fact about lcm of powers of two with 45, yielding the iff RSCounting_Gap45_Absolute D ↔ D = 3. The present theorem sits in a separate Hopf-linking section and takes a topological route instead of the counting route.
The named hypothesis asserts the biconditional: a natural number equals 3 exactly when there exists a strictly positive real equal to the Hopf linking penalty. That penalty is the cost attached to irreducible, non-trivial linking of 1-spheres (Hopf-type). The hypothesis is still marked scaffold, with an explicit TODO to prove that the linking number is an invariant only in dimension three for 1-spheres.
Elsewhere in the monolith the spatial dimension constant is hard-wired to 3 and documented as forced by T8 (or T9 linking). This declaration packages that linking requirement as an explicit implication from penalty existence to $D=3$.
proof idea
Pure term-mode one-liner. Introduce the dimension $D$ and the existence witness for a positive Hopf linking penalty. Apply the reverse direction of the uniqueness hypothesis at that $D$: the hypothesis supplies $D=3 \leftrightarrow$ (exists positive penalty equal to the Hopf linking penalty), so the right-to-left arrow turns the witness into $D=3$. No arithmetic, no unfolding of the penalty constant.
why it matters
Places the classical Hopf-linking argument for three-space inside the Recognition forcing chain (primer landmark T8: $D=3$ spatial dimensions; related comments call it T9 linking). It is the thin bridge from the scaffolded uniqueness proposition to a usable implication "positive linking penalty $\Rightarrow D=3$".
The same module already forces $D=3$ via RSCounting and the absolute 45-gap; this declaration is the parallel linking-based witness. No downstream consumers are wired yet (used_by is empty), so its role is presently local: keep the linking story theorem-shaped while the uniqueness hypothesis remains open.
Closing the scaffold (prove linking number is only a non-trivial invariant for 1-spheres in $D=3$, and that $D=2$ and $D=4$ fail as the sibling hypotheses suggest) would discharge the hypothesis and make this implication unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.