spinorDim3
plain-language theorem explainer
The fundamental spinor representation in three spatial dimensions is two-dimensional. Anyone citing the Cl₃ ≅ M₂(ℂ) or Spin(3) ≅ SU(2) bridge statements uses this constant as the forced carrier size. It is a one-line definition fixing the classical formula 2^{⌊D/2⌋} at D = 3.
Claim. The dimension of the fundamental spinor representation of $\mathrm{Spin}(3)$ is $2$. Equivalently, for spatial dimension $D = 3$ one has $2^{\lfloor D/2 \rfloor} = 2$.
background
The module CliffordBridge links Recognition Science's eight-tick cadence to Clifford algebras and Bott periodicity. Main claims include Cl_{n+8} ≅ Cl_n ⊗ Cl_8, the identification of the 8-tick DFT grading with Cl₈, and the spin-group bridge Spin(3) ≅ SU(2) in D = 3.
Upstream, spatial dimension is fixed at D = 3 by the forcing chain (T8 / T9): linking and the recognition event configuration force three spatial directions. The classical spinor dimension formula is 2^{⌊D/2⌋}; at D = 3 this evaluates to 2, matching the two-component Weyl/Pauli spinors of non-relativistic 3D quantum mechanics and the fundamental of SU(2).
Sibling material in the same file treats Cl₃ (Clifford algebra of Euclidean 3-space), its period-8 Bott structure, and the Euclidean quadratic forms used to present those algebras.
proof idea
Pure definition: the natural number is set equal to 2. No tactics or lemmas. Downstream theorems such as spinor_two_component simply unfold this definition by rfl, and certificate structures assert spinorDim3 = 2 as a field.
why it matters
This constant is the numeric anchor for the spinor side of the Clifford–RS bridge. Cl3IsoM2C records that the forced spinor carrier is the two-component complex carrier and that dim(Cl₃) = 8 matches dim_ℝ(M₂(ℂ)). Spin3IsoSU2 requires spinor_dimension : spinorDim3 = 2 and ties Spin(3) ⊂ Cl₃⁺ ≅ ℍ to unit quaternions ≅ SU(2). The theorem spinor_two_component is the trivial equality spinorDim3 = 2, and CliffordBridgeCert bundles the whole bridge (including period 8).
In the Recognition framework this sits under T8 (D = 3) and the eight-tick octave: once space is three-dimensional, spin-½ and the SU(2) gauge structure are forced by the Clifford algebra of that space, not put in by hand. It does not itself prove Bott periodicity or the full algebra isomorphism; those live in the surrounding certificate structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.