D3_has_linking
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 in Recognition Science
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.
scope and limits
- Does not derive D=3 from the eight-tick period or gap-45 synchronization.
- Does not construct explicit links or compute their linking numbers.
- Does not address higher homotopy groups or other topological invariants.
- Does not treat physical realizations or stability of links under deformation.
Lean usage
example : SupportsNontrivialLinking 3 := D3_has_linkingformal statement (Lean)
287theorem D3_has_linking : SupportsNontrivialLinking 3 :=
proof body
Term-mode proof.
288 (alexander_duality_circle_linking 3).mpr rfl
289
290/-- **T8 PRIMARY THEOREM**: Linking requires D = 3.
291 Proof: Alexander duality — no reference to 8-tick or gap-45. -/