clifford_dimension
plain-language theorem explainer
Records that the real vector-space dimension of the Clifford algebra Cl_n is the power 2^n. Cited by anyone wiring the 8-tick DFT grading to Cl_8 or checking that Cl_3 is eight-dimensional. The proof is pure definitional equality (rfl) on natural-number exponentiation.
Claim. For every natural number $n$, $2^n = 2^n$. In context this is the standard dimension count: $\dim_{\mathbb{R}}(\mathrm{Cl}_n) = 2^n$.
background
The module CliffordBridge links Recognition Science's eight-tick structure to classical Clifford algebra and Bott periodicity. Main aims stated in the module header: Cl_{n+8} ≅ Cl_n ⊗ Cl_8, the 8-tick DFT grading matching Cl_8, and Spin(3) ≅ SU(2) for D = 3 spinors.
Classically, the Clifford algebra Cl_n on an n-dimensional real quadratic space has basis the ordered products of distinct generators, hence real dimension 2^n. Sibling declarations in the file name Cl3, Cl8, the Euclidean quadratic forms in dimensions 3 and 8, and the Bott period equal to eight.
Upstream edges reported by the graph (CircleWindingChain injectivity of winding, ContinuumBridge Laplacian identification) are not used in the proof body; the statement is self-contained arithmetic.
proof idea
Term-mode one-liner: both sides of the equality are the same natural-number power, so rfl closes the goal by definitional equality. No lemmas are applied. The theorem name and doc-comment supply the Clifford interpretation; the Lean proposition itself is only the numeral identity.
why it matters
Gives the dimension yardstick used throughout the Clifford bridge: Cl_3 is 8-dimensional and Cl_8 is 256-dimensional as real vector spaces. That 8 matches the eight-tick octave forced at T7 in the UnifiedForcingChain and the Bott period recorded by sibling results (cliffordPeriod_eq_eight, bottPeriodicity).
The module frames Bott periodicity and the Cl_8 grading isomorphism as the reason RS needs exactly eight ticks (spinor period 8, KO-theory period 8, division-algebra period 8). This dimension fact is the elementary counting step behind those claims. No downstream users are recorded yet; it stands as a named anchor for later Cl_3 / Cl_8 constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.