spinor_dim_D1

formal source

 192theorem spinor_dim_D3 : spinorDimension 3 = 2 := rfl
 193
 194/-- D = 1 gives 1-component (trivial) spinors. -/
 195theorem spinor_dim_D1 : spinorDimension 1 = 1 := rfl
 196
 197/-- D = 2 gives 2-component spinors (but SO(2) is abelian). -/
 198theorem spinor_dim_D2 : spinorDimension 2 = 2 := rfl
 199
 200/-- D = 4 gives 4-component spinors (chiral structure). -/
 201theorem spinor_dim_D4 : spinorDimension 4 = 4 := rfl
 202
 203/-- A dimension has the RS-required spinor structure if:
 204    1. Spinors are 2-component (spin-½ particles)
 205    2. Spin(D) is non-abelian (for gauge interactions)
 206    3. Spin(D) is simple (not a product)
 207
 208    **Scope note**: This structure describes D=3 as having the right Clifford/spinor
 209    properties (Cl₃ ≅ M₂(ℂ), Spin(3) ≅ SU(2)). It is a *characterization* of why
 210    D=3 is physically special, not the derivation. The formal proof that D=3 is
 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