dimC
plain-language theorem explainer
The speed of light has dimension exponents (0, 1, −1) in the (M, L, T) basis, i.e. dimensions [L T⁻¹]. Anyone assembling or citing the c–ℏ–G dimension matrix uses this vector as the first row. It is a literal three-component rational assignment, not a derived claim.
Claim. In the $(M,L,T)$ exponent basis, the dimensional signature of the speed of light $c$ is the rational vector $(0,1,-1)$, i.e. dimensions $[L\,T^{-1}]$.
background
This module is a kernel-checked no-go certificate: in the classical mass–length–time basis the three dimensionful constants $c$, $\hbar$, and $G$ have exponent vectors
$$c\colon(0,1,-1),\quad \hbar\colon(1,2,-1),\quad G\colon(-1,3,-2).$$
Linear independence of those vectors over $\mathbb{Q}$ means the only dimensionless monomial $c^a\hbar^b G^g$ is the trivial one. The module therefore separates legitimate RS targets (dimensionless outputs such as mass ratios or $\alpha$) from category errors of the form “the framework derives the SI value of $\hbar$.”
Upstream, Dimension structures elsewhere track $(L,T,M)$ or spatial $D$; here the local convention is the ordered triple $(M,L,T)$ as rational coordinates on $\mathrm{Fin},3$. Native RS identities $c=1$, $\hbar_R=\varphi^{-5}$, $G_R=\varphi^5/\pi$ fix units inside the theory; they are not SI predictions.
proof idea
Pure definition: the function $\mathrm{Fin},3\to\mathbb{Q}$ is the vector literal $![0,1,-1]$. No lemmas, tactics, or computation. Index $0$ is the mass exponent, $1$ length, $2$ time.
why it matters
This vector is the first row of the dimension matrix whose determinant is $-2$. Downstream, that matrix feeds dimMatrix_det, the no-go theorem no_dimensionless_combination (only $a=b=g=0$ yields a dimensionless monomial), and the referee-facing corollary si_values_not_derivable_from_pure_numbers.
In the Recognition framework this is the local obstruction that keeps SI values of $c$, $\hbar$, and $G$ outside the pure-number fragment of the theory. It sharpens the primer distinction: native units ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) are definitions of the RS yardstick, not derivations of CODATA numbers. Dimensionless targets (forcing chain T5–T8 outputs, $\alpha$ band, mass ratios on the $\varphi$-ladder) remain in scope; this file only walls off the dimensionful SI triple.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.