dimMatrix
plain-language theorem explainer
The 3×3 rational matrix whose rows are the (M,L,T) dimension-exponent vectors of c, ℏ, and G. Anyone arguing linear independence of those three constants' dimensions cites this packing. It is assembled by stacking the three pre-defined exponent vectors; no computation lives here.
Claim. Define the $3\times 3$ matrix $D$ over $\mathbb{Q}$ whose rows are the dimension-exponent vectors of $c$, $\hbar$, and $G$ in the $(M,L,T)$ basis: row 1 is $(0,1,-1)$, row 2 is $(1,2,-1)$, row 3 is $(-1,3,-2)$.
background
This module is a local no-go certificate: 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)$. If the matrix they form has nonzero determinant, the only dimensionless monomial $c^a\hbar^b G^g$ is the trivial one.
The three row vectors are named separately: dimC, dimHbar, and dimG (each a map Fin 3 → ℚ). A parallel integer matrix with transposed basis order $(L,T,M)$ lives in NativeDimensionalBoundary; both packings serve the same independence argument. The module stresses that native identities such as $\hbar_R=\varphi^{-5}$ and $G_R=\varphi^5/\pi$ fix units, not SI predictions.
proof idea
Pure definitional packing. Matrix.of stacks the three already-defined row vectors dimC, dimHbar, dimG into a Matrix (Fin 3) (Fin 3) ℚ. No lemmas, no tactics, no arithmetic.
why it matters
This matrix is the data object behind the dimensional-rigidity no-go. Downstream, dimMatrix_det evaluates its determinant as $-2$, and no_dimensionless_combination turns $\det\neq 0$ into the statement that only the zero exponents yield a dimensionless monomial. The same matrix (or its integer twin) feeds dimension_matrix_c_hbar_G_det_nonzero and the certificate structure NativeDimensionalBoundaryCert.
In Recognition Science terms the result fences the framework: dimensionless targets (mass ratios, $\alpha$, eight-tick counts, $D=3$) remain legitimate; claims that a pure-number theory "derives" the SI values of $c$, $\hbar$, or $G$ are category errors. Native units still set $\hbar=\varphi^{-5}$ and $G=\varphi^5/\pi$ by definition, calibrated to SI by one external anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.