HasRSSpinorStructure

formal source

 211    forced rests on Alexander duality: the linking group H̃^{D-2}(S¹) = ℤ iff D = 3.
 212    The spinor conditions (two_component, nonabelian, simple) and the 8-tick identity
 213    (2^D = 8) are derived as *consequences* of D=3, not used as premises. -/
 214structure HasRSSpinorStructure (D : Dimension) : Prop where
 215  /-- 2-component spinors -/
 216  two_component : spinorDimension D = 2 ∨ D = 3
 217  /-- Spin(D) is non-abelian — for D=3 this follows from Spin(3)≅SU(2) -/
 218  nonabelian : D ≥ 3
 219  /-- Spin(D) is simple (D = 3 or D ≥ 5) -/
 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