dimMatrix_det
plain-language theorem explainer
The 3×3 matrix of (M,L,T) exponent vectors for (c, ℏ, G) has determinant −2. Anyone invoking the dimensional no-go for SI constants in Recognition Science cites this exact evaluation (or its nonvanishing corollary). The proof unfolds the three columns, applies the closed 3×3 determinant formula, and finishes by numeric normalization.
Claim. Let $D$ be the $3\times 3$ integer matrix whose columns are the $(M,L,T)$ dimension vectors of $c$, $\hbar$, and $G$. Then $\det D = -2$.
background
In the (M, L, T) basis the three dimensionful constants carry exponent vectors $c:(0,1,-1)$, $\hbar:(1,2,-1)$, $G:(-1,3,-2)$. Stacking them produces an integer matrix whose invertibility over $\mathbb{Q}$ decides whether any nontrivial monomial $c^a\hbar^b G^g$ can be dimensionless.
The module DimensionalRigidity is a kernel-checked no-go certificate: because that matrix has nonzero determinant, the only dimensionless combination is the trivial one $(a,b,g)=(0,0,0)$. The present lemma records the concrete value of the determinant used by every downstream independence argument.
Native RS identities such as $\hbar_R=\varphi^{-5}$ and $G_R=\varphi^5/\pi$ fix values inside recognition units; they are definitions of the unit system, not predictions of SI numbers. An external anchor is always required to reach SI.
proof idea
Short term-mode proof. Unfold the dimension matrix together with the three column
definitions (exponents of $c$, $\hbar$, and $G$), invoke Mathlib's closed formula
for the determinant of a $3\times 3$ matrix, and discharge the resulting integer
arithmetic by norm_num. No deeper lemmas are required.
why it matters
Computational heart of the dimensional-rigidity certificate. Downstream,
dimension_matrix_c_hbar_G_det_nonzero rewrites through this equality and obtains
$\det\neq 0$, hence linear independence of the three exponent vectors over
$\mathbb{Q}$ and the no-go: the only dimensionless monomial in $c$, $\hbar$, $G$
is the trivial one.
In Recognition Science the result closes the $\hbar/G$ audit's category-error finding as a proved boundary stone. Dimensionless targets ($\alpha$, mass ratios, $g_\star$-type counts) remain legitimate; SI values of the three dimensionful constants cannot be derived from pure numbers alone. The value $-2$ (rather than $\pm 1$) also records that $(c,\hbar,G)$ span an index-$2$ sublattice of the integer dimension lattice, so the Planck system is a basis only up to half-integer powers; the boundary argument itself needs only nonvanishing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.