m2c_real_dimension
plain-language theorem explainer
The real vector-space dimension of the 2-by-2 complex matrix algebra is eight, recorded as the arithmetic identity 2·2·2=8. Anyone wiring the Cl₃ ≅ M₂(ℂ) leg of the T8 spinor bridge cites this count. The proof is pure reflexivity: Lean reduces both sides definitionally.
Claim. As a real vector space, $M_2(\mathbb{C})$ has dimension $2\cdot 2\cdot 2=8$ (two rows, two columns, and two real coordinates per complex entry).
background
The CliffordBridge module links Recognition Science's eight-tick structure to Clifford algebras and Bott periodicity. Main landmarks are Cl_{n+8} ≅ Cl_n ⊗ Cl_8, the identification of the 8-tick DFT grading with Cl₈, and the spinor bridge at spatial dimension D=3.
At D=3 one has the classical isomorphism Cl₃ ≅ M₂(ℂ). The complex matrix algebra M₂(ℂ) is four-dimensional over ℂ; each complex entry contributes two real coordinates, so the underlying real dimension is eight. That count matches both 2³ (the Clifford dimension of Cl₃) and the eight-tick octave forced by T7/T8.
Upstream constants fix D := 3 (AlphaDerivation, GapDerivation). Downstream certificates package Cl₃ ≅ M₂(ℂ), Spin(3) ≅ SU(2), spinor dimension 2^{⌊3/2⌋}=2, and Clifford dimension 2³=8 into a single T8 bridge.
proof idea
Term-mode one-liner: rfl. Both sides of 2 * 2 * 2 = 8 are closed natural-number numerals, so definitional reduction closes the goal with no lemmas and no tactics.
why it matters
Feeds the T8 → canonical spinor bridge in UnifiedForcingChain. That certificate requires, among other fields, the Clifford dimension 2³=8 and the Cl₃ ≅ M₂(ℂ) isomorphism; this identity is the arithmetic witness that the real dimension of M₂(ℂ) equals the Clifford dimension of Cl₃ and the eight-tick period.
In the forcing chain, T8 forces D=3 spatial dimensions and T7 forces the eight-tick octave. Bott periodicity (period 8) and the real spinor period then sit on the same integer. The parent theorem t8_to_canonical_spinor_bridge_holds assembles Cl₃ ≅ M₂(ℂ), Spin(3) ≅ SU(2), spinor dimension 2, and this dimension count into one Prop under T8_Dimension_Forced.
Without the real-dimension match, the M₂(ℂ) model would not line up with the 8-tick/Cl₈ grading story the module is built to justify.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.