dimHbar
plain-language theorem explainer
Planck's constant carries the (M,L,T) exponent vector (1, 2, −1), i.e. dimensions M L² T⁻¹. Anyone assembling the (c, ℏ, G) dimension matrix or proving linear independence of those three vectors cites this row. The body is a three-component rational vector literal, not a derived computation.
Claim. In the mass-length-time basis, the dimensional exponent vector of $\hbar$ is $(1, 2, -1)$, corresponding to $[\mathrm{M}\,\mathrm{L}^{2}\,\mathrm{T}^{-1}]$.
background
The module DimensionalRigidity is a local no-go certificate: in the (M, L, T) basis the three SI-dimensionful constants c, ℏ, G have exponent vectors that are linearly independent over ℚ, so the only dimensionless monomial c^a ℏ^b G^g is the trivial one. The native RS identities ℏ_R = φ⁻⁵ and G_R = φ⁵/π are unit definitions, not SI predictions.
Each constant is recorded as a map Fin 3 → ℚ giving its (M, L, T) exponents. For ℏ the classical mechanical dimensions are mass × length² × time⁻¹, hence the vector (1, 2, −1). Sibling vectors are dimC = (0, 1, −1) and dimG = (−1, 3, −2).
Upstream Dimension structures elsewhere in the codebase track L, T, M exponents for bookkeeping; here the three-slot Fin 3 encoding is fixed once so the matrix of rows can be formed and its determinant computed over ℚ.
proof idea
Pure definition: the vector is the Mathlib array literal ![1, 2, -1] of type Fin 3 → ℚ. No lemmas, tactics, or computation are involved. Index 0 is the mass exponent, index 1 length, index 2 time.
why it matters
This row is the middle input to dimMatrix (the 3×3 matrix with rows dimC, dimHbar, dimG). That matrix feeds dimMatrix_det, which proves det = −2 ≠ 0, and thereby the kernel theorem no_dimensionless_combination: if a·dim(c) + b·dim(ℏ) + g·dim(G) = 0 componentwise then a = b = g = 0.
The corollary si_values_not_derivable_from_pure_numbers restates the obstruction for referees: a pure-number framework cannot output the SI value of c, ℏ, or G individually, because no nontrivial dimensionless combination exists to fix a scale. The module doc frames this as closing the ℏ/G audit's category-error finding as a kernel-checked boundary stone. It does not touch T0–T8 forcing, RCL, or dimensionless RS targets (mass ratios, α, g⋆ counts).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.