D4_no_spinor_structure

formal source

 237  norm_num at hna
 238
 239/-- D = 4 does not have RS spinor structure (product Spin(4) ≅ SU(2) × SU(2)). -/
 240theorem D4_no_spinor_structure : ¬HasRSSpinorStructure 4 := by
 241  intro ⟨htwo, _, hsimple⟩
 242  cases hsimple with
 243  | inl h3 => norm_num at h3
 244  | inr h5 => norm_num at h5
 245
 246/-- The unique dimension with RS spinor structure AND 8-tick is D = 3.
 247
 248    This replaces the linking axiom with a Clifford algebra-based characterization.
 249    The proof uses:
 250    1. RS requires 8-tick = 2^D, so D must divide into 2³
 251    2. RS requires non-abelian simple Spin(D)
 252    3. Only D = 3 satisfies both -/
 253theorem spinor_eight_tick_forces_D3 (D : Dimension)
 254    (_ : HasRSSpinorStructure D)
 255    (h_eight : EightTickFromDimension D = eight_tick) : D = 3 :=
 256  eight_tick_forces_D3 D h_eight
 257
 258/-! ## The Linking Argument (Via Alexander Duality — Independent of T7)
 259
 260D = 3 is the unique dimension admitting non-trivial linking of closed curves.
 261This is a theorem of algebraic topology (Alexander duality), fully independent
 262of the 8-tick structure.
 263
 264`SupportsNontrivialLinking D := SphereAdmitsCircleLinking D` uses the
 265cohomology-based predicate from `AlexanderDuality.lean`. The equivalence
 266`SphereAdmitsCircleLinking D ↔ D = 3` is a genuine theorem proved from
 267the reduced cohomology axiom for S¹, not a definitional identity.
 268
 269**Bidirectional forcing (no circularity):**
 270- T8: Alexander duality → D = 3  (independent of T7)