dimension_matrix_c_hbar_G_det_nonzero
plain-language theorem explainer
The (c, ℏ, G) dimension matrix has nonzero determinant, so the three dimension vectors are linearly independent over ℤ. Anyone arguing that pure dimensionless RS data cannot fix absolute SI values of ℏ or G cites this. The proof rewrites by the already-computed det = −2 and finishes by norm_num.
Claim. Let $M$ be the $3\times 3$ integer matrix whose columns are the $(L,T,M)$ exponent vectors of $c=(1,-1,0)$, $\hbar=(2,-1,1)$, and $G=(3,-2,-1)$. Then $\det M \neq 0$.
background
This module draws the honest line between first-principles native constants and SI calibration. RS forces dimensionless identities such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$, but cannot output absolute SI values of $\hbar$ or $G$ from pure dimensionless data: a dimensional bridge needs a dimensional anchor.
The matrix in play is dimMatrix, with columns the length-time-mass exponent vectors of $c$, $\hbar$, and $G$. Upstream, dimMatrix_det evaluates $\det=-2$ by expanding the $3\times 3$ determinant. The value $-2$ (not $\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 only needs nonvanishing.
Native $G$ and $\hbar$ appear as RS projections ($G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$, $\hbar=E_{\mathrm{coh}}\tau_0$), not as CODATA SI numbers. The positive half of the story (one anchor suffices and uniquely determines the bridge) lives in SIBridgeClosure and SingleAnchor.
proof idea
One-line term-mode wrapper. Rewrite the goal with dimMatrix_det (which states $\det=-2$), then close $\neq 0$ by norm_num. No matrix algebra is re-derived here.
why it matters
Feeds native_dimensional_boundary_cert, the module certificate that native constants are first-principles only up to the dimensional boundary and that SI conversion is uniquely constrained calibration once an anchor is supplied. The certificate wires this nonvanishing determinant together with no_nontrivial_dimensionless_monomial and si_bridge_is_calibration_not_prediction.
In the framework this is the negative half of dimensional analysis: because $\det\neq 0$, no nontrivial monomial $c^a\hbar^b G^d$ is dimensionless, so pure RS dimensionless data cannot fix absolute SI scales. The positive half (one anchor $\tau_0$ determines the full bridge, including the electron mass in SI kilograms via the T0–T8 capstone) is already formalized elsewhere. Together: exactly one dimensional anchor, and it determines everything. Landmark contact is the SI bridge around the native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, not a new forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.