pith. machine review for the scientific record. sign in
theorem proved term proof

spinor_dim_D4

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 201theorem spinor_dim_D4 : spinorDimension 4 = 4 := rfl

proof body

Term-mode proof.

 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. -/

depends on (27)

Lean names referenced from this declaration's body.