no_dimensionless_combination
plain-language theorem explainer
The only rational exponents making c^a ℏ^b G^g dimensionless are a = b = g = 0. Anyone arguing that a pure-number framework cannot derive SI values of c, ℏ, or G cites this linear-independence fact over (M,L,T). The proof specializes the three component equations, unfolds the explicit dimension vectors, and finishes by linear arithmetic.
Claim. If $a,b,g\in\mathbb{Q}$ satisfy $a\,\mathrm{dim}(c)+b\,\mathrm{dim}(\hbar)+g\,\mathrm{dim}(G)=0$ componentwise in the $(M,L,T)$ basis, then $a=b=g=0$. Equivalently, the only dimensionless monomial $c^a\hbar^b G^g$ is the trivial one.
background
In the mass-length-time dimension basis the three SI constants carry exponent vectors $c:(0,1,-1)$, $\hbar:(1,2,-1)$, and $G:(-1,3,-2)$. The module records these componentwise as maps on $\mathrm{Fin},3$.
The local setting is a no-go certificate for dimensional rigidity. The $3\times 3$ matrix of those vectors has determinant $-2\neq 0$, so they are linearly independent over $\mathbb{Q}$: the only dimensionless monomial $c^a\hbar^b G^g$ is the trivial one. A framework whose outputs are pure numbers can therefore never derive the SI values of $c$, $\hbar$, or $G$ individually.
Native RS identities such as $\hbar_R=\varphi^{-5}$ and $G_R=\varphi^5/\pi$ are definitions of native units, not SI predictions. The module isolates this local obstruction about dimensionful constants and leaves dimensionless targets (mass ratios, $\alpha$, etc.) untouched.
proof idea
Specialize the hypothesis at the three indices of $\mathrm{Fin},3$ to obtain three scalar equations. Unfold the dimension vectors for $c$, $\hbar$, and $G$ (with $\mathrm{Fin.isValue}$) by simp, producing an explicit homogeneous $3\times 3$ system over $\mathbb{Q}$. Conclude $a=b=g=0$ by three linarith goals on the simplified equations. No external lemmas beyond the local dimension definitions are required.
why it matters
Direct input to the corollary that SI values are not derivable from pure numbers: that result assumes a nontrivial rational triple with vanishing weighted dimension sum, applies this theorem, and obtains a contradiction. The module frames the pair as resolving the $\hbar/G$ audit category-error finding as a kernel-checked boundary stone.
In Recognition Science the result protects the split between native-unit definitions ($\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ from the constants layer) and SI calibration through an external anchor. Dimensionless outputs remain legitimate targets; this no-go only blocks claims that SI values of dimensionful constants are framework-derived. It is local to $(c,\hbar,G)$ and does not touch the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.