spinorDimension
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the value of D itself.
- Does not prove the Clifford algebra isomorphism for D=3.
- Does not handle non-integer or negative dimensions.
- Does not incorporate the length-time-mass exponents from Constants.Dimension.
Lean usage
theorem spinor_dim_D3 : spinorDimension 3 = 2 := rflformal statement (Lean)
189def spinorDimension (D : Dimension) : ℕ := 2^(D / 2)
proof body
Definition body.
190
191/-- D = 3 gives 2-component spinors. -/