theorem
proved
term proof
why_D_equals_3
show as:
view Lean formalization →
formal statement (Lean)
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 :=
proof body
Term-mode proof.
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
456
457 See `AlexanderDuality.alexander_duality_circle_linking` for the
458 topological proof from the S¹ cohomology axiom. -/