cl3_iso_m2c
plain-language theorem explainer
A concrete certificate that the Clifford algebra of Euclidean 3-space matches 2×2 complex matrices at the level of finite carriers, real dimension 8, and two-component spinors. Anyone citing the D=3 spinor bridge or the complete 8-tick Clifford package uses this witness. The body is a three-field structure instance: cast equivalences plus a reflexivity proof of 2³=8.
Claim. There is a packaged witness that $\mathrm{Cl}_3 \cong M_2(\mathbb{C})$ in the Recognition sense: the finite real carriers are equivalent ($\mathrm{Fin}(2^3) \simeq \mathrm{Fin}(2\cdot 2\cdot 2)$), the dimension identity $2^3 = 8 = \dim_{\mathbb{R}} M_2(\mathbb{C})$ holds, and the forced spinor carrier is the two-component complex space $(\mathrm{Fin}\,2 \to \mathbb{C})$.
background
The module links Recognition Science's eight-tick register to Clifford algebra and Bott periodicity. Main landmarks are $\mathrm{Cl}_{n+8}\cong\mathrm{Cl}_n\otimes\mathrm{Cl}_8$, the identification of the 8-tick DFT grading with $\mathrm{Cl}_8$, and the spin bridge $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$ forced at spatial dimension $D=3$.
The structure being inhabited packages three finite checks rather than a full algebra isomorphism object: matching eight-dimensional real carriers, the numerical identity $\dim\mathrm{Cl}3=2^3=8=\dim{\mathbb{R}}M_2(\mathbb{C})$, and a nonempty equivalence of the spinor carrier with $\mathbb{C}^2$. Its doc-comment stresses why this matters: spin-½, the $\mathrm{SU}(2)$ gauge structure, and the quaternion picture $\mathbb{H}\oplus\mathbb{H}$.
Upstream, the same module already records Bott periodicity and the DFT–Clifford grading bridge; this definition supplies the $D=3$ matrix-algebra side of that story.
proof idea
Definitional construction of a three-field structure value. The carrier equivalence is Equiv.cast justified by norm_num on the finite cardinals $2^3$ and $2\cdot 2\cdot 2$. The dimension field is pure reflexivity (rfl). The spinor-carrier field is again Equiv.cast with a reflexivity proof that the named spinor dimension at $D=3$ is $2$. No external lemmas beyond those tactics; it is a direct witness, not a derived theorem.
why it matters
This is the named API surface that replaced an old True placeholder for $\mathrm{Cl}_3\cong M_2(\mathbb{C})$. It is plugged directly into the complete 8-tick Clifford bridge package (cl3_iso := cl3_iso_m2c) and into the forcing-chain certificate T8_To_CanonicalSpinor_Bridge, whose doc-comment states that at $D=3$ the Clifford algebra is canonically $M_2(\mathbb{C})$ with spinor dimension $2^{\lfloor 3/2\rfloor}=2$ and Clifford dimension $2^3=8$.
In the Recognition forcing chain this sits under T8 (spatial dimension forced to 3) and the eight-tick octave (T7): once $D=3$ is fixed, the spinor and matrix pictures are no longer free choices. Downstream t8_to_canonical_spinor_bridge_holds simply assigns this witness to the bridge field. It does not itself prove Bott periodicity or $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$; those are sibling fields of the same bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.