pith. machine review for the scientific record. sign in
theorem proved term proof high

spinor_dim_D3

show as:
view Lean formalization →

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.

claimIn 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 192theorem spinor_dim_D3 : spinorDimension 3 = 2 := rfl

proof body

Term-mode proof.

 193
 194/-- D = 1 gives 1-component (trivial) spinors. -/

depends on (1)

Lean names referenced from this declaration's body.