si_values_not_derivable_from_pure_numbers
plain-language theorem explainer
A pure-number framework cannot derive the SI values of c, ℏ, or G individually. Any such claim would need a nontrivial dimensionless monomial in those three constants, and none exists over the rationals. Referees auditing SI-value claims in Recognition Science (or any dimensionless theory) cite this no-go. The proof unpacks the existential and applies linear independence of the (M,L,T) exponent vectors.
Claim. There do not exist rationals $a,b,g$, not all zero, such that $a\,\mathrm{dim}(c)+b\,\mathrm{dim}(\hbar)+g\,\mathrm{dim}(G)=0$ componentwise in the $(M,L,T)$ basis. Equivalently, the only dimensionless monomial $c^{a}\hbar^{b}G^{g}$ has $a=b=g=0$.
background
In the mass-length-time basis the three SI constants carry exponent vectors $c:(0,1,-1)$, $\hbar:(1,2,-1)$, $G:(-1,3,-2)$. The module records these as the maps $\mathrm{dim}(c)$, $\mathrm{dim}(\hbar)$, $\mathrm{dim}(G)$ on $\mathrm{Fin},3$.
The local setting is a no-go certificate: the $3\times 3$ matrix with those rows has determinant $-2\neq 0$, so the vectors are linearly independent over $\mathbb{Q}$. Hence the only dimensionless monomial $c^{a}\hbar^{b}G^{g}$ is the trivial one.
Upstream, the theorem on no dimensionless combination states: if $a,\mathrm{dim}(c)+b,\mathrm{dim}(\hbar)+g,\mathrm{dim}(G)=0$ componentwise, then $a=b=g=0$. The present corollary restates that obstruction in the direction referees quote: SI values of dimensionful constants are not pure-number outputs of a dimensionless framework.
proof idea
Short term-mode proof by contradiction. Introduce the existential witness $(a,b,g)$ together with the nontriviality hypothesis and the componentwise vanishing condition. Apply the upstream no-dimensionless-combination theorem to conclude $a=b=g=0$. A one-line simplification then contradicts nontriviality of $(a,b,g)$.
why it matters
Makes the category-error finding from the ℏ/G audit a kernel-checked boundary stone (module dated 2026-07-06). Recognition Science fixes native identities $\hbar_{R}=\varphi^{-5}$ and $G_{R}=\varphi^{5}/\pi$ as definitions of units, not as SI predictions; this theorem formalizes why those cannot be read as SI derivations. Dimensionless targets remain legitimate: mass ratios on the $\varphi$-ladder, $\alpha^{-1}$ inside $(137.030,137.039)$, and $g_{\star}$-type counts. No downstream dependents yet; the declaration stands as a verification certificate rather than a stepping-stone lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.