D1_no_spinor_structure
plain-language theorem explainer
Recognition Science excludes one-dimensional space from supporting the required spinor structure for spin-1/2 particles and non-abelian interactions. Model builders in dimensional reduction scenarios cite this to discard D=1. The proof obtains an immediate contradiction by assuming the structure and applying numerical normalization to the non-abelian field.
Claim. Dimension one fails the RS spinor structure: it admits neither two-component spinors nor non-abelian Spin(D) nor a simple Spin(D) group.
background
The module proves spatial dimension is forced to three by topological and synchronization constraints. HasRSSpinorStructure(D) is the structure requiring two-component spinors (spinorDimension D = 2 or D = 3), non-abelian Spin(D) (D ≥ 3), and simple Spin(D) (D = 3 or D ≥ 5). The module documentation states that only D = 3 supports stable topological conservation via non-trivial linking, while D = 1 has no room for linking.
proof idea
The term proof introduces the assumed HasRSSpinorStructure 1. This supplies the nonabelian hypothesis D ≥ 3. Normalization then yields the immediate contradiction 1 ≥ 3.
why it matters
This negative case eliminates D = 1 inside the linking argument for dimension forcing. It supports the module claim that only D = 3 satisfies both topological conservation and the spinor requirements (Cl_3 ≅ M_2(C), Spin(3) ≅ SU(2)). The result feeds the broader eight-tick and gap-45 synchronization that isolates D = 3 via 2^D = 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.