dimMatrix_det
plain-language theorem explainer
The integer dimension matrix whose columns are the (L,T,M) exponent vectors of c, ħ, and G has determinant exactly −2. Anyone arguing that no nontrivial monomial c^a ħ^b G^d is dimensionless cites this evaluation. The proof is a direct three-by-three determinant expansion via simp on the explicit matrix entries.
Claim. Let $M$ be the $3\times 3$ integer matrix whose columns are the length-time-mass exponent vectors of $c=(1,-1,0)$, $\hbar=(2,-1,1)$, and $G=(3,-2,-1)$. Then $\det M = -2$.
background
This module draws the honest line between RS-native dimensionless identities and SI calibration. Native relations such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$ are forced inside the framework; absolute SI values of $\hbar$ or $G$ are not. A dimensional bridge therefore needs an external anchor.
The object here is the classical dimension matrix of $(c,\hbar,G)$. Columns are the $(L,T,M)$ exponent vectors $c=(1,-1,0)$, $\hbar=(2,-1,1)$, $G=(3,-2,-1)$, written as the integer matrix $M=\begin{pmatrix}1&2&3\-1&-1&-2\0&1&-1\end{pmatrix}$.
Linear independence of those three vectors is the standard dimensional-analysis fact that no nontrivial monomial $c^a\hbar^b G^d$ is dimensionless. The determinant value itself is stronger than mere nonvanishing: $\det=-2$ means $(c,\hbar,G)$ span an index-$2$ sublattice of $\mathbb{Z}^3$, so the Planck system is a basis only up to half-integer powers.
proof idea
Term-mode proof by simplification. Unfold dimMatrix to the explicit Matrix.of of three Fin 3 columns, then apply Mathlib's Matrix.det_fin_three together with the standard cons/of_apply accessors. The resulting integer arithmetic evaluates to $-2$; no external lemmas about constants or physics are required.
why it matters
Feeds the immediate corollary dimension_matrix_c_hbar_G_det_nonzero (det ≠ 0), which is the linear-independence statement used to prove there is no nontrivial dimensionless monomial in $c$, $\hbar$, and $G$. That no-go is the negative half of the native dimensional boundary: pure dimensionless RS data cannot fix absolute SI scales, so exactly one dimensional anchor is required.
Also re-exported (or paralleled) in Verification.DimensionalRigidity.dimMatrix_det, where the same evaluation underwrites the rigidity/no-go package. Together with the positive half already formalized in SIBridgeClosure and SingleAnchor (one anchor determines the full bridge), this closes the "exactly one anchor" story that the module doc records. Framework landmark: the RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ live on the dimensionless side; this lemma is why they cannot jump the SI boundary alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.