spinorDimension
plain-language theorem explainer
Spinor dimension is defined as 2 raised to the floor of D over 2 for each spatial dimension D. Researchers checking spin-1/2 representations against the RS ledger would cite this when confirming that D=3 produces exactly two components. The definition is a direct arithmetic expression with no lemmas or reductions applied.
Claim. The spinor dimension in spatial dimension $D$ is $2^{D/2}$ (integer division).
background
In the DimensionForcing module spatial dimension is an alias for the natural numbers. The module proves D=3 is forced by topological linking (non-trivial knots only in three dimensions) and by synchronization of the eight-tick cycle with the 45-tick cumulative phase. Upstream the Constants.Dimensions.Dimension structure records length-time-mass exponents, but the local Dimension here is simply the integer count of spatial directions.
proof idea
Direct definition. The body is the arithmetic expression 2^(D/2) using integer division; no tactics or upstream lemmas are invoked.
why it matters
This supplies the spinor-dimension function used by HasRSSpinorStructure to verify that D=3 yields two-component spinors while satisfying non-abelian and simplicity conditions. It supports the eight-tick forcing of D=3 (T7 in the primer) and the claim that only D=3 gives the Clifford algebra Cl_3 ≅ M_2(ℂ) required for RS gauge structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.