spinor_dim_D3
plain-language theorem explainer
For spatial dimension three, the Clifford spinor-dimension formula evaluates to two. Anyone citing the T8-to-canonical-spinor bridge or the D=3 forcing package needs this numerical identity. The proof is pure definitional equality: natural floor-division gives floor(3/2)=1, hence 2^1=2.
Claim. The spinor dimension formula $2^{\lfloor D/2 \rfloor}$ at $D=3$ equals $2$.
background
In Clifford algebra, the (complex) spinor representation of $\mathrm{Spin}(D)$ has dimension $2^{\lfloor D/2 \rfloor}$. This module builds the bridge from Recognition Science's eight-tick structure to Bott periodicity of Clifford algebras; when spatial dimension is three one has $\mathrm{Cl}_3 \cong M_2(\mathbb{C})$, which supplies two-component spinors.
The local definition encodes that count by natural division (floor): $\mathrm{spinorDimFormula}(D)=2^{D/2}$. Upstream constants fix $D:=3$ as the forced spatial dimension (T8 / linking, hypercube vertex count $2^D$). Module commentary lists why three is special: $\mathrm{Cl}_3 \cong M_2(\mathbb{C})$, $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$, nontrivial $\pi_1(\mathrm{SO}(3))$, and nontrivial knot theory only in $D=3$.
proof idea
One-line term proof by reflexivity. Unfolding the formula reduces the goal to $2^{(3/2)}=2$ in $\mathbb{N}$. Natural division sends $3/2$ to $1$, and $2^1$ reduces to $2$, so both sides are definitionally equal and rfl closes.
why it matters
Supplies the numerical half of the T8 Clifford/spinor bridge. Downstream, t8_to_canonical_spinor_bridge_holds packages this fact as spinor_dim_at_D3 together with $\mathrm{Cl}_3\cong M_2(\mathbb{C})$ and $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$, so that the forcing chain step "T8 supplies the canonical Clifford/spinor bridge" is fully witnessed.
A parallel identity lives in DimensionForcing (spinor dimension at three equals two). Framework landmark: T8 forces three spatial dimensions; this pins the resulting two-component spinors that match the Pauli/$\mathrm{SU}(2)$ structure used in ordinary quantum mechanics and in the eight-tick Bott story of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.