D3SpinorUniqueness
plain-language theorem explainer
Bundles three elementary identities that pin D = 3 as the unique spatial dimension linking two-component spinors to the eight-tick cycle: spinor dimension 2^{⌊3/2⌋} = 2, hypercube order 2^3 = 8, and Clifford period equal to that order. Anyone citing the Clifford–RS bridge or Spin(3) ≅ SU(2) spinor structure will pull this record. The witness is pure definitional equality (rfl on each field).
Claim. A record asserting three facts for spatial dimension $D = 3$: the spinor-dimension formula gives $2^{\lfloor 3/2 \rfloor} = 2$ (two-component complex spinors); $2^3 = 8$ (the $D$-hypercube has eight vertices); and the Clifford Bott period equals $2^3$, matching the recognition eight-tick period.
background
The module links Recognition Science's forced eight-tick octave to classical Clifford algebra via Bott periodicity: $\mathrm{Cl}_{n+8} \cong \mathrm{Cl}_n \otimes \mathrm{Cl}_8$, with the 8-tick DFT grading identified with the grading of $\mathrm{Cl}_8$, and $\mathrm{Spin}(3) \cong \mathrm{SU}(2)$ supplying the $D=3$ spinor structure.
Upstream, spatial dimension is fixed at $D = 3$ by the forcing chain (T8 / linking). The spinor-dimension formula is $2^{\lfloor D/2 \rfloor}$, so at $D=3$ one obtains complex two-spinors. The Clifford period is the constant $8$, the same integer as the recognition period $2^D$ when $D=3$. Together these make $D=3$ the first nonzero dimension whose hypercube order coincides with Bott's period.
proof idea
Not a proof object: a structure packing three propositional fields. The canonical witness fills each field by rfl against the definitions spinorDimFormula, natural-number power, and cliffordPeriod := 8. No lemmas are invoked; the content is definitional equality of naturals.
why it matters
Feeds the complete 8-tick–Clifford bridge bundle, which requires Bott periodicity, the DFT–Clifford mode map, and the $\mathrm{Cl}_3 \cong M_2(\mathbb{C})$ spinor structure. It records why T8's $D=3$ is not an extra assumption relative to the eight-tick octave (T7): $2^3 = 8$ is exactly the Clifford/Bott period, and the same $D$ yields the minimal nontrivial complex spinors used by $\mathrm{Spin}(3) \cong \mathrm{SU}(2)$. Framework landmarks: T7 eight-tick octave, T8 $D=3$, and the module's Bott-periodicity bridge. No open scaffold; the equalities are closed by definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.