spinorDimFormula
plain-language theorem explainer
The irreducible spinor dimension in D spatial dimensions is written as the closed form 2^{⌊D/2⌋}. Anyone citing the D=3 Clifford/spinor bridge or the T8 forcing step uses this as the dimension count. It is a one-line natural-number definition (integer division supplies the floor).
Claim. For any spatial dimension $D \in \mathbb{N}$, the spinor dimension is $\mathrm{dim} = 2^{\lfloor D/2 \rfloor}$. In particular, at the forced value $D = 3$ one has $2^{\lfloor 3/2 \rfloor} = 2$.
background
The module links Recognition Science's eight-tick cadence to Clifford algebra and Bott periodicity. Main landmarks are Cl_{n+8} ≅ Cl_n ⊗ Cl_8, the identification of the 8-tick DFT grading with Cl_8, and the spin-group bridge Spin(3) ≅ SU(2) that supplies spinors in three spatial dimensions.
Across the forcing chain the spatial dimension is fixed at D = 3 (T8 / T9). Upstream constants simply set D := 3 as that forced value. The classical formula for the (complex) spinor dimension of Cl_D is 2^{⌊D/2⌋}; at D = 3 this yields two-component spinors, matching Cl_3 ≅ M_2(ℂ).
Integer division on ℕ implements the floor, so the definition is exactly the textbook count used by the D=3 uniqueness certificate and the T8-to-spinor bridge.
proof idea
Pure definition: the body is the single term 2^(D / 2). On natural numbers, / is floor division, so this is 2^{⌊D/2⌋} with no further proof obligations. Downstream equalities such as the D=3 specialization are discharged by rfl.
why it matters
This is the dimension count that makes D = 3 special in the Clifford bridge. It is required by the D=3 spinor-uniqueness certificate (complex_spinors: the formula at 3 equals 2), by the direct specialization theorem that records spinorDimFormula 3 = 2, and by the T8-to-canonical-spinor bridge in the unified forcing chain, which surfaces 2^{⌊3/2⌋} = 2 together with Cl_3 ≅ M_2(ℂ), Spin(3) ≅ SU(2), Clifford dimension 2^3 = 8, and Bott period 8.
That package feeds the extended ultimate-inevitability theorem, closing the spinor side of the T8 (D = 3) step. Framework landmarks: T8 forces three spatial dimensions; the eight-tick octave matches Bott period 8 and 2^D at D = 3. Without this formula the spinor half of the Clifford bridge has no dimension to cite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.