rather
plain-language theorem explainer
In the (M,L,T) basis the exponent vectors of c, ℏ, and G are linearly independent over ℚ (matrix determinant −2), so the only dimensionless monomial is the trivial one. Cite this as the kernel-checked no-go against deriving SI values of dimensionful constants from a pure-number framework. The argument is elementary lattice linear algebra on the three exponent columns.
Claim. Write the dimension vectors $c=(0,1,-1)$, $\hbar=(1,2,-1)$, $G=(-1,3,-2)$ in the $(M,L,T)$ basis. The $3\times 3$ integer matrix they form has $\det=-2\neq 0$, hence the vectors are linearly independent over $\mathbb{Q}$. Equivalently, $c^a\hbar^b G^g$ is dimensionless if and only if $a=b=g=0$. Native identities such as $\hbar_R=\varphi^{-5}$ and $G_R=\varphi^5/\pi$ fix units; they are not SI predictions.
background
Dimensional Rigidity is a verification no-go (dated 2026-07-06) that turns a category-error finding from the ℏ/G audit into a checked boundary stone. Physical dimensions are tracked by the Dimension structure: integer exponents $(L,T,M)$ for length, time, and mass.
In SI-style units the three classical constants carry $c:[L T^{-1}]$, $\hbar:[M L^2 T^{-1}]$, $G:[M^{-1} L^3 T^{-2}]$. Stacking those exponent triples as columns (or rows) yields an integer matrix whose non-vanishing determinant means they span a full-rank sublattice of $\mathbb{Z}^3$.
The module is explicit about scope: this blocks derivation of dimensionful SI values from any framework whose outputs are pure numbers. Dimensionless targets (mass ratios, $\alpha$, $g_\star$-type counts) remain legitimate. Upstream, RS already fixes native units via the forcing chain ($\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ in RS units with $c=1$); those are unit definitions, not external predictions.
proof idea
Form the $3\times 3$ integer matrix whose columns are the $(M,L,T)$ exponent vectors of $c$, $\hbar$, and $G$. Evaluate its determinant; the value is $-2\neq 0$. Non-zero determinant over $\mathbb{Z}$ (hence over $\mathbb{Q}$) implies linear independence of the three vectors, so the only rational solution of $a,v_c+b,v_\hbar+g,v_G=0$ is $a=b=g=0$. That is exactly the statement that the only dimensionless monomial $c^a\hbar^b G^g$ is the trivial one.
Sibling declarations in the module package the vectors (dimC, dimHbar, dimG), the matrix, its determinant, and the corollaries no_dimensionless_combination and si_values_not_derivable_from_pure_numbers. The same matrix appears downstream as NativeDimensionalBoundary.dimMatrix (with the note that $\lvert\det\rvert=2$ records an index-2 sublattice).
why it matters
This file is the official answer to claims of the form "the framework derives ℏ" or "derives G": such claims are category errors once dimensions are tracked. RS may fix $\hbar_R=\varphi^{-5}$ and $G_R=\varphi^5/\pi$ as definitions of native units (primer constants with $c=1$) and must still calibrate to SI through one external anchor.
Downstream consumers include NativeDimensionalBoundary.dimMatrix (the shared dimension matrix and det $-2$ fact), electroweak VEV ledger structure, $\lambda$ balance uniqueness, and baryogenesis staging carriers that inherit dimensional bookkeeping. The no-go deliberately leaves dimensionless RS targets untouched: $\alpha$ in the $(137.030,137.039)$ band, mass-ladder ratios, and counting factors remain the legitimate derivation surface. It closes the audit gap by making the obstruction a theorem-shaped boundary rather than prose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.