physical_eight_tick

formal source

 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.
 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) ∧