cHbarGDimension
plain-language theorem explainer
Maps integer exponents of a monomial in c, ħ, and G to the resulting length-time-mass dimension triple. Anyone proving that no nontrivial combination of these three constants is dimensionless cites this linear map. The body is the explicit combination of the classical dimension vectors of c, ħ, and G; there is no proof content beyond the definition.
Claim. For integers $a,b,d$, the dimension exponents $(L,T,M)$ of the monomial $c^{a}\hbar^{b}G^{d}$ equal $(a+2b+3d,\,-a-b-2d,\,b-d)$, using the classical assignments $c\sim L T^{-1}$, $\hbar\sim M L^{2} T^{-1}$, and $G\sim L^{3} M^{-1} T^{-2}$.
background
The module records the honest boundary between first-principles native constants and SI calibration. Recognition Science can force 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 alone. A dimensional bridge needs a dimensional anchor.
Classical dimensional analysis assigns $c$ the vector $(1,-1,0)$, $\hbar$ the vector $(2,-1,1)$, and $G$ the vector $(3,-2,-1)$ in $(L,T,M)$ exponent space. A monomial $c^{a}\hbar^{b}G^{d}$ then has total dimension equal to the integer linear combination of those three columns.
Upstream, the RS-native $G$ is the recognition/Planck projection $\lambda_{\mathrm{rec}}^{2}c^{3}/(\pi\hbar)$, and native $\hbar$ is $E_{\mathrm{coh}}\cdot\tau_{0}=\varphi^{-5}$. This definition only packages their SI dimension vectors for the independence argument that follows.
proof idea
Pure definition with no lemmas. The three output components are the matrix-vector product of the classical $(c,\hbar,G)$ dimension matrix (columns $(1,-1,0)$, $(2,-1,1)$, $(3,-2,-1)$) with the exponent column $(a,b,d)^{\top}$. Equivalently, the body is the explicit linear combination $a\cdot(1,-1,0)+b\cdot(2,-1,1)+d\cdot(3,-2,-1)$.
why it matters
Feeds the key negative result of the module: no nontrivial monomial in $c$, $\hbar$, and $G$ is dimensionless (no_nontrivial_dimensionless_monomial), and therefore a pure-number theory needs a dimensional anchor (dimensionless_theory_needs_anchor). Both facts are packaged into the audit certificate NativeDimensionalBoundaryCert.
This is the dimensional-analysis half of the SI-bridge story. The positive half (one anchor suffices and determines the bridge uniquely) already lives in SIBridgeClosure and SingleAnchor; together they justify that exactly one dimensional anchor determines everything. Framework landmarks $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$ in RS-native units sit on the other side of this boundary: native identities are forced, absolute SI values are not.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.