D3_has_spinor_structure
plain-language theorem explainer
Dimension 3 satisfies the RS spinor structure, which requires two-component spinors, a non-abelian spin group, and a simple spin group. Researchers working on dimension selection in Recognition Science cite this result inside the forcing arguments of the Foundation.DimensionForcing module. The proof is a direct term construction that instantiates the three fields of the structure via reflexivity on equality and the order relation.
Claim. The dimension $D=3$ satisfies the RS spinor structure: spinorDimension $D=2$ or $D=3$, $D$ is at least 3, and $D=3$ or $D$ is at least 5.
background
The DimensionForcing module shows that spatial dimension equals 3 is forced by the Recognition Science framework. It combines a topological linking argument (only D=3 permits stable knots and links for conservation) with an 8-tick synchronization condition whose least common multiple with 45 yields the 360-degree periodicity of SO(3). The structure HasRSSpinorStructure D : Prop encodes three properties: two_component asserts spinorDimension D = 2 or D = 3; nonabelian requires D ≥ 3; simple requires D = 3 or D ≥ 5. This matches the Clifford algebra isomorphism Cl_3 ≅ M_2(ℂ) and Spin(3) ≅ SU(2). The upstream lemma le_refl states that n ≤ n for any LogicNat n and supplies the witness for the nonabelian field.
proof idea
The proof is a term-mode construction of the HasRSSpinorStructure instance. It supplies two_component by the right disjunct and reflexivity on D=3, nonabelian by the reflexivity lemma le_refl applied to 3, and simple by the left disjunct and reflexivity on D=3.
why it matters
The declaration sits inside the dimension-forcing results of Foundation.DimensionForcing and supplies one concrete characterization of why D=3 is physically distinguished. It aligns with the T8 step of the unified forcing chain that selects three spatial dimensions and with the module's 8-tick/45-tick synchronization that produces the observed 360-degree rotational periodicity. No downstream theorems are recorded, leaving open how this spinor characterization will be invoked in later ledger or particle constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.