why_D_equals_3

formal source

 422
 423    The Alexander duality argument is the logically primary route.
 424    Items 2–5 are consequences or characterizations, not premises. -/
 425theorem why_D_equals_3 :
 426    -- Spinor structure requires D = 3
 427    (∀ D, HasRSSpinorStructure D → EightTickFromDimension D = 8 → D = 3) ∧
 428    -- Eight-tick requires D = 3
 429    (∀ D, EightTickFromDimension D = 8 → D = 3) ∧
 430    -- Unique compatible dimension
 431    (∃! D, RSCompatibleDimension D) ∧
 432    -- That dimension is 3
 433    D_physical = 3 :=
 434  ⟨spinor_eight_tick_forces_D3, eight_tick_forces_D3, dimension_forced, rfl⟩
 435
 436/-! ## Summary -/
 437
 438/-- **DIMENSION FORCING SUMMARY**
 439
 440    D = 3 is not chosen, it is forced:
 441
 442    | Argument               | Role          | Independence         |
 443    |------------------------|---------------|----------------------|
 444    | Alexander duality      | PRIMARY PROOF | Independent of T7    |
 445    | 2-component spinors    | characterizes | consequence of D = 3 |
 446    | Spin(D) ≅ SU(2)        | characterizes | consequence of D = 3 |
 447    | 8-tick = 2^D           | consequence   | follows from D = 3   |
 448    | lcm(8,45) = 360        | consequence   | follows from 8-tick  |
 449
 450    The spatial dimension of the universe is a theorem, not an axiom.
 451
 452    **Key insight (T7/T8 circularity resolved):**
 453    - T8 (D = 3) is proved from Alexander duality ALONE
 454    - T7 (period = 8) follows as a consequence: D = 3 → 2^D = 2^3 = 8
 455    - The linking predicate is genuinely cohomological, not D = 3 in disguise