SupportsNontrivialLinking
plain-language theorem explainer
SupportsNontrivialLinking D asserts that the D-sphere admits non-trivial linking of disjoint embedded circles, witnessed by nonzero linking number in the complement. Researchers deriving spatial dimension from topological conservation in Recognition Science cite this predicate to separate the linking property from any reference to the eight-tick period. The definition is a one-line wrapper around SphereAdmitsCircleLinking.
Claim. A natural number $D$ supports nontrivial linking of closed curves when the sphere $S^D$ admits two disjoint embedded circles with nonzero linking number, equivalently when the reduced cohomology group satisfies $H̃^{D-2}(S^1) ≅ ℤ$.
background
The DimensionForcing module proves that spatial dimension equals 3 via four arguments, the first being topological. Dimension is the natural number type. SphereAdmitsCircleLinking D is defined via CircleReducedCohomologyNontrivial (D-2), which by Alexander duality (Hatcher Thm 3.44) equals the condition that $H̃_1(S^D ∖ S^1) ≅ H̃^{D-2}(S^1)$ is nontrivial precisely for D=3. The module doc states that only D=3 supports stable topological conservation because D=1 is collinear, D=2 separates by the Jordan theorem, and D≥4 unlinks by general position.
proof idea
This is a one-line wrapper that applies SphereAdmitsCircleLinking to the input dimension D.
why it matters
This definition supplies the topological predicate used by linking_requires_D3 (SupportsNontrivialLinking D → D=3) and D3_has_linking (SupportsNontrivialLinking 3). It fills the linking argument of the Dimension Forcing module and provides the T8 foundation that D=3 without reference to the eight-tick octave or gap-45 synchronization. The module doc notes that only D=3 permits information that cannot be unlinked by continuous deformation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.