spinor_dim_D2
plain-language theorem explainer
The spinor dimension equals two when the spatial dimension is two. Researchers examining the Recognition Science arguments that force D=3 would cite this baseline to contrast the abelian SO(2) case against the non-abelian structure required for stable topological conservation. The equality follows immediately by reflexivity from the definition of spinor dimension as two to the power of floor of D over two.
Claim. The spinor dimension in two spatial dimensions satisfies $2 = 2$, where the spinor dimension in $D$ dimensions is defined by $2^{D/2}$.
background
The Dimension Forcing module proves that spatial dimension D equals three by four independent arguments. The topological linking argument shows that only D=3 supports non-trivial conservation under continuous deformation: D=1 is collinear, D=2 unlinks by the Jordan curve theorem, and D greater than or equal to 4 unlinks by codimension. The spinor dimension is defined in the same module as spinorDimension(D) := 2^(D/2), which yields the standard two-component spinors for D=2.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of spinorDimension at argument 2.
why it matters
This baseline supports the dimension-forcing chain by supplying the D=2 case where spinors remain two-component yet SO(2) is abelian. It contributes to the overall argument that only D=3 yields both non-trivial topology and the eight-tick octave (T7, T8) required by the Recognition Science framework. The result sits alongside siblings such as eight_tick_forces_D3 and power_of_2_forces_D3 that complete the forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.