HasRSSpinorStructure
plain-language theorem explainer
A spatial dimension D carries the RS spinor structure when its spinors are two-component, the spin group is non-abelian, and the spin group is simple. Researchers deriving D=3 from Clifford algebra requirements for spin-1/2 particles and gauge interactions would cite this characterization. The declaration is a structure definition that directly packages the three conditions on D.
Claim. A dimension $D$ has the RS spinor structure when $2^{D/2}=2$ or $D=3$, when $D≥3$, and when $D=3$ or $D≥5$.
background
The module DimensionForcing establishes that spatial dimension equals 3 by combining topological linking with an 8-tick synchronization condition. Dimension is the type of natural numbers. spinorDimension D is defined as 2 to the power of floor D over 2. The structure requires two-component spinors for spin-1/2 particles, a non-abelian spin group for gauge interactions, and a simple spin group that is not a product group.
proof idea
This is a structure definition that directly assembles the three conditions into a single Prop. No lemmas or tactics are applied; the fields two_component, nonabelian, and simple are stated verbatim from the spinorDimension definition and the numerical inequalities on D.
why it matters
The structure is used by D3_has_spinor_structure, D1_no_spinor_structure, D2_no_spinor_structure, D4_no_spinor_structure, spinor_eight_tick_forces_D3, and why_D_equals_3. It supplies the Clifford algebra side of the argument that only D=3 satisfies both the spinor requirements and the eight-tick period from T7, complementing the Alexander duality linking argument that forces D=3 independently of the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.