D_physical

formal source

 390/-! ## Physical Interpretation -/
 391
 392/-- The spatial dimension of the physical world. -/
 393def D_physical : Dimension := 3
 394
 395/-- D_physical is RS-compatible. -/
 396theorem D_physical_compatible : RSCompatibleDimension D_physical := D3_compatible
 397
 398/-- The eight-tick cycle in D = 3 dimensions. -/
 399theorem physical_eight_tick : EightTickFromDimension D_physical = 8 := rfl
 400
 401/-- **WHY D = 3**
 402
 403    The dimension is not a free parameter. It is forced by:
 404
 405    1. **Alexander duality (PRIMARY, proved from axiom)**:
 406       `SphereAdmitsCircleLinking D ↔ D = 3`, proved from the reduced
 407       cohomology of S¹ axiom in `AlexanderDuality.lean`. Independent of T7.
 408       H̃₁(Sᴰ \ S¹) ≅ H̃^{D-2}(S¹), nontrivial iff D = 3.
 409
 410    2. **Clifford algebra (CHARACTERIZATION)**: Cl₃ ≅ M₂(ℂ) gives
 411       2-component complex spinors — the unique structure for spin-½.
 412       (See `CliffordBridge.cl3_iso_m2c`)
 413
 414    3. **Spin group (CHARACTERIZATION)**: Spin(3) ≅ SU(2) is the simplest
 415       non-abelian compact Lie group (gauge structure for weak interactions).
 416
 417    4. **Bott periodicity (CONSEQUENCE)**: Period 8 = 2³ = 2^D follows
 418       from D = 3, linking Clifford periodicity to dimension.
 419
 420    5. **Gap-45 (CONSEQUENCE)**: lcm(8, 45) = 360 = 2³ × 3² × 5 follows
 421       from the 8-tick = 2^3 derived from D = 3.
 422
 423    The Alexander duality argument is the logically primary route.