D3_has_spinor_structure

formal source

 220  simple : D = 3 ∨ D ≥ 5
 221
 222/-- D = 3 has the RS spinor structure. -/
 223theorem D3_has_spinor_structure : HasRSSpinorStructure 3 := {
 224  two_component := Or.inr rfl
 225  nonabelian := le_refl 3
 226  simple := Or.inl rfl
 227}
 228
 229/-- D = 1 does not have RS spinor structure (too few dimensions). -/
 230theorem D1_no_spinor_structure : ¬HasRSSpinorStructure 1 := by
 231  intro ⟨_, hna, _⟩
 232  norm_num at hna
 233
 234/-- D = 2 does not have RS spinor structure (abelian rotations). -/
 235theorem D2_no_spinor_structure : ¬HasRSSpinorStructure 2 := by
 236  intro ⟨_, hna, _⟩
 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)