Linking requires D = 3 (Alexander duality)
Non-trivial linking of closed curves exists in S^D if and only if D = 3. This follows from Alexander duality: H̃₁(S^D \ S¹) ≅ H̃^{D-2}(S¹; ℤ) is nontrivial precisely when D-2 = 1. The predicate SphereAdmitsCircleLinking D encodes this via CircleReducedCohomologyNontrivial, and alexander_duality_circle_linking proves the biconditional. Consequently linking_requires_D3 shows SupportsNontrivialLinking D → D = 3, with D = 1,2,≥4 ruled out by the same theorem.
8-tick = 2^D forces D = 3
The eight-tick period is defined as EightTickFromDimension D := 2^D. The theorem eight_tick_forces_D3 states that EightTickFromDimension D = eight_tick implies D = 3, proved by reducing to power_of_2_forces_D3 which exhausts cases D ≠ 3 by direct computation and growth bounds.
Cl_3 spinor structure
Clifford algebra Cl_D yields spinorDimension D = 2^{⌊D/2⌋}. Only D = 3 produces 2-component complex spinors with Spin(3) ≅ SU(2) (non-abelian and simple). This is witnessed by spinor_dim_D3, D3_has_spinor_structure, and the negation theorems for D = 1,2,4; the structure is compatible with the 8-tick identity only at D = 3.
Cited Lean anchors
The load-bearing theorems are eight_tick_forces_D3, linking_requires_D3, alexander_duality_circle_linking, and D3_has_spinor_structure in IndisputableMonolith.Foundation.DimensionForcing.