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

spinor_dim_D1

show as:
view Lean formalization →

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.

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

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.

scope and limits

formal statement (Lean)

 195theorem spinor_dim_D1 : spinorDimension 1 = 1 := rfl

proof body

Term-mode proof.

 196
 197/-- D = 2 gives 2-component spinors (but SO(2) is abelian). -/

depends on (5)

Lean names referenced from this declaration's body.