H_D4TrivialLinking
plain-language theorem explainer
Scaffold hypothesis: in spatial dimension D ≥ 4, any two closed curves can be unlinked by an ambient isotopy (linking is topologically trivial). Dimension-rigidity arguments cite it to rule out D ≥ 4 as a home for nontrivial hopf-type linking. The body is a placeholder Prop (universally True), not a proved topology theorem.
Claim. For every natural number $D \geq 4$ and any two curves, those curves are ambient-isotopic to an unlinked pair. (Present formalization: a placeholder proposition that holds for all such $D$ and dummy curve data.)
background
The Verification.Dimension module shows that RSCounting plus 45-gap synchronization forces spatial dimension $D = 3$, with the iff form RSCounting_Gap45_Absolute $D \leftrightarrow D = 3$. The argument is kept arithmetic-light (lcm and RecogSpec facts) for PrimeClosure.
Linking supplies the geometric reason $D = 3$ is special. Upstream constants fix $D := 3$ as the spatial dimension forced by the T8/T9 chain (linking requires three dimensions). Sibling hypotheses cover the complementary cases: no linking in $D = 2$, and uniqueness of nontrivial linking in $D = 3$.
Classical differential topology: in codimension high enough ($D \geq 4$), 1-dimensional submanifolds can be isotoped apart; knotted and linked 1-cycles become trivial under ambient isotopy. That is the intended content of this hypothesis.
proof idea
No proof. The declaration is a def of a Prop whose body is the constant-true predicate over $D \geq 4$ and dummy Unit curve slots. A commented axiom line marks where a real assumption would be installed. Closing the scaffold means replacing the placeholder with a formal ambient-isotopy statement (and either proving it from Mathlib topology or accepting a named axiom).
why it matters
In the Recognition forcing chain, T8 forces $D = 3$ spatial dimensions; T9-style linking language appears in AlphaDerivation as "linking requires $D = 3$". This hypothesis is the $D \geq 4$ half of that geometric dichotomy: if linking is always trivial above three dimensions, then only $D = 3$ can carry the nontrivial hopf-type linking penalty used by dimensional rigidity witnesses in this module.
Siblings H_D2NoLinking and H_ThreeDimensionalLinkingUnique complete the case split. Downstream use is not yet wired (used_by empty); the module's proved core is the RSCounting/45-gap arithmetic route to $D = 3$. This scaffold is the topology-side story that would justify why higher-$D$ worlds drop out of recognition geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.