dimG
plain-language theorem explainer
Dimension exponent vector of Newton's constant G in the (M, L, T) basis: (−1, 3, −2), i.e. M⁻¹ L³ T⁻². Anyone building the (c, ℏ, G) dimension matrix for the dimensional-rigidity no-go cites this row. It is a pure definition: the three rational components are written out as a Fin 3 → ℚ vector.
Claim. The dimension exponent vector of Newton's gravitational constant $G$ in the $(M,L,T)$ basis is $(-1, 3, -2)$, corresponding to the SI dimensions $[M^{-1} L^{3} T^{-2}]$.
background
The module DimensionalRigidity is a local no-go certificate: in the classical (M, L, T) basis the three dimensionful constants c, ℏ, G carry fixed exponent vectors, and the claim is that those vectors are linearly independent over ℚ. Consequently the only dimensionless monomial c^a ℏ^b G^g is the trivial one.
This declaration supplies the third row. By standard dimensional analysis, G has dimensions M⁻¹ L³ T⁻², so its exponent triple is (−1, 3, −2). Sibling rows are dimC = (0, 1, −1) and dimHbar = (1, 2, −1). The three rows are stacked into dimMatrix.
Upstream names G appear in Constants (RS-native G = λ_rec² c³/(π ℏ)), Codata (SI CODATA value), and cost/inflaton reparametrizations; none of those enter the vector itself. The vector is pure dimensional bookkeeping, independent of the RS-native numerical identities ℏ_R = φ⁻⁵ and G_R = φ⁵/π.
proof idea
Definition, not a theorem. The body is the Fin-vector literal ![-1, 3, -2], i.e. the map sending 0 ↦ −1, 1 ↦ 3, 2 ↦ −2 on Fin 3. No lemmas or tactics are involved.
why it matters
This row is the third ingredient of dimMatrix := Matrix.of ![dimC, dimHbar, dimG]. That matrix has determinant −2 (dimMatrix_det), hence is invertible over ℚ. Linear independence immediately yields no_dimensionless_combination: if a·dim(c) + b·dim(ℏ) + g·dim(G) = 0 componentwise then a = b = g = 0. The referee-facing corollary si_values_not_derivable_from_pure_numbers follows at once: a pure-number framework cannot output the SI value of c, ℏ, or G individually, because no nontrivial dimensionless combination exists to fix a scale.
In the RS framework this closes the ℏ/G audit category-error finding as a kernel-checked boundary stone. Native identities such as G_R = φ⁵/π remain definitions of units, not SI predictions; the legitimate targets stay dimensionless (mass ratios, α, g⋆-type counts). The result is local to dimensionful constants and does not touch the forcing chain T0–T8 or the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.