dimMatrix
plain-language theorem explainer
Explicit 3×3 integer matrix whose columns are the (L,T,M) exponent vectors of c, ℏ, and G. Anyone arguing that the Planck triad is dimensionally independent cites this object. The body is a pure matrix literal (no proof).
Claim. Define the $3\times 3$ integer matrix $D$ whose columns are the length-time-mass exponent vectors of $c=(1,-1,0)$, $\hbar=(2,-1,1)$, and $G=(3,-2,-1)$: $$D=\begin{pmatrix}1&2&3\\-1&-1&-2\\0&1&-1\end{pmatrix}.$$
background
The module draws the honest line between RS-native dimensionless identities and SI calibration. RS can force relations such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$, but pure dimensionless data cannot fix absolute SI values of $\hbar$ or $G$; a dimensional anchor is required.
In classical dimensional analysis each quantity carries an integer exponent triple in (length, time, mass). Here $c$ has dimensions $LT^{-1}$, $\hbar$ has $L^{2}T^{-1}M$, and $G$ has $L^{3}T^{-2}M^{-1}$. Stacking those three vectors as columns yields the matrix above.
Upstream constants supply the RS-native and CODATA projections of $G$ and $\hbar$, but this definition only records the exponent lattice data, not numerical values.
proof idea
Definition, not a theorem. The body is Matrix.of applied to the explicit Fin 3 → Fin 3 → ℤ array with rows $(1,2,3)$, $(-1,-1,-2)$, $(0,1,-1)$. No lemmas or tactics are involved.
why it matters
This matrix is the carrier for the module's negative half of the dimensional-boundary argument: an anchor is required. Downstream, dimMatrix_det evaluates $\det D=-2$, and dimension_matrix_c_hbar_G_det_nonzero records $\det\neq 0$, hence linear independence of the three dimension vectors. That independence feeds no_nontrivial_dimensionless_monomial and the certificate NativeDimensionalBoundaryCert.
The same matrix (over $\mathbb{Q}$) reappears in Verification.DimensionalRigidity, where the no-go theorem states that no nontrivial monomial $c^{a}\hbar^{b}G^{d}$ is dimensionless. Together with the positive half already proved in SIBridgeClosure and SingleAnchor (one scalar $\tau_{0}$ determines the full bridge), this closes the "exactly one dimensional anchor" story that sits under the T0–T8 to SI capstone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.