spinor_dim_D3
plain-language theorem explainer
The declaration establishes that the spinor dimension equals two when the spatial dimension is fixed at three. Researchers deriving Clifford algebra representations or Dirac operators inside the Recognition Science framework would cite this equality to confirm consistency with standard 3D spinors. The proof reduces immediately by reflexivity to the definition of spinor dimension as two raised to the floor of D over two.
Claim. In three spatial dimensions the spinor representation has dimension two: $2^{3/2} = 2$.
background
The DimensionForcing module proves that spatial dimension D equals three is forced by the Recognition Science framework. It uses topological linking (non-trivial knots only in D=3) and synchronization between the eight-tick cycle (2^D) and the gap-45 cumulative phase, yielding the 360-degree periodicity that selects D=3 uniquely. Spinor dimension is introduced as the function that returns two to the power of the floor of D divided by two, matching the standard count of independent components in the spinor representation.
proof idea
The proof is a one-line term that applies reflexivity directly to the definition of spinorDimension evaluated at D=3, which computes to 2 via integer division.
why it matters
This equality confirms that the forced D=3 from the eight-tick octave and T8 step produces the expected two-component spinors used in quantum mechanics. It closes a consistency check inside the dimension-forcing chain without introducing new hypotheses. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.