256 eight_tick_forces_D3 D h_eight 257 258/-! ## The Linking Argument (Via Alexander Duality — Independent of T7) 259 260D = 3 is the unique dimension admitting non-trivial linking of closed curves. 261This is a theorem of algebraic topology (Alexander duality), fully independent 262of the 8-tick structure. 263 264`SupportsNontrivialLinking D := SphereAdmitsCircleLinking D` uses the 265cohomology-based predicate from `AlexanderDuality.lean`. The equivalence 266`SphereAdmitsCircleLinking D ↔ D = 3` is a genuine theorem proved from 267the reduced cohomology axiom for S¹, not a definitional identity. 268 269**Bidirectional forcing (no circularity):** 270- T8: Alexander duality → D = 3 (independent of T7) 271- T7: D = 3 → period = 2^3 = 8 (uses D from T8) 272- Neither presupposes the other. -/ 273 274/-- A dimension supports non-trivial linking of closed curves. 275 276 **Genuine topological definition**: whether Sᴰ admits disjoint 277 S¹-embeddings with nonzero linking number, as determined by 278 Alexander duality (H̃₁(Sᴰ \ S¹) ≅ H̃^{D-2}(S¹) ≅ ℤ iff D = 3). 279 280 This replaces the previous circular definition (2^D = 8) with a 281 predicate that is independent of the 8-tick period. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.