spinor_dim_D1
plain-language theorem explainer
The declaration shows that the spinor dimension equals one for a single spatial dimension, matching the trivial one-component case. Researchers examining base cases in the Recognition Science dimension-forcing arguments would cite this to anchor the D=1 entry in the topological linking analysis. The proof is a direct reflexivity step on the definition of spinor dimension.
Claim. The spinor dimension in one spatial dimension equals 1, i.e., $2^{1/2} = 1$ where the exponent uses floor division.
background
The DimensionForcing module establishes that only D=3 permits stable topological conservation through non-trivial linking of curves. For D=1 every configuration remains collinear with no room for linking; for D=2 the Jordan curve theorem forces every closed curve to bound a disk and unlink; for D>=4 codimension arguments again allow unlinking. The spinor dimension is defined upstream as 2 to the power of floor(D/2).
proof idea
The proof is a one-line term-mode reflexivity that matches the definition of spinor dimension directly for input 1, where floor division of 1 by 2 yields exponent 0 and 2^0 equals 1.
why it matters
This base case anchors the D=1 entry in the four-argument forcing chain that isolates D=3 via the eight-tick octave (2^D) and the 45-tick cumulative phase synchronization whose lcm yields 360. It supplies the trivial spinor endpoint against which the D=3 case (two-component spinors) is contrasted in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.