D3_has_linking
plain-language theorem explainer
Dimension three supports non-trivial linking of closed curves, witnessed by the Hopf link with linking group isomorphic to the integers. Recognition Science researchers cite the result to anchor the topological case for D=3 in the forcing chain. The proof is a one-line term application of Alexander duality at D=3 that discharges the goal by reflexivity.
Claim. $D=3$ supports non-trivial linking of closed curves: there exist disjoint embeddings of $S^1$ into $S^3$ with nonzero linking number, equivalently the reduced homology satisfies $H̃_1(S^3 ∖ S^1) ≅ ℤ$.
background
The DimensionForcing module proves that spatial dimension D=3 is forced by the RS framework. Its first argument is topological: only D=3 permits stable conservation via non-trivial linking of closed curves. SupportsNontrivialLinking D is defined as SphereAdmitsCircleLinking D, the predicate that S^D admits disjoint S^1-embeddings whose linking number is nonzero, as detected by Alexander duality on the complement.
proof idea
The proof is the term (alexander_duality_circle_linking 3).mpr rfl. It invokes the upstream equivalence SphereAdmitsCircleLinking D ↔ D=3 at the concrete value 3, applies the right-to-left direction, and closes the resulting equality with reflexivity.
why it matters
D3_has_linking supplies the linking field of the parent theorem D3_compatible, which asserts that dimension 3 is RS-compatible. The declaration realizes the primary linking argument of the module and aligns with T8 of the unified forcing chain that selects D=3. It is deliberately independent of the eight-tick period, furnishing a purely topological justification within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
3D scene tokens raise diffusion robot policy to new SOTA on RLBench
"We unify these two lines of work and present 3D Diffuser Actor, a neural policy equipped with a novel 3D denoising transformer that fuses information from the 3D visual scene"
-
Higher-form symmetries organize anomalies and gauging in QFT
"p-form symmetries combine to form a p-form symmetry group G(p)... Ug(Σd-p-1)Ug′(Σd-p-1) = Ugg′(Σd-p-1)"