native_dimensional_boundary_cert
plain-language theorem explainer
Packages the dimensional-boundary audit: the (c, ℏ, G) dimension vectors are linearly independent, no nontrivial monomial in them is dimensionless, and the SI tick-square map is a positive injective calibration in the anchor. Cite it when separating first-principles native identities from SI conversion. Term-mode structure inhabitant wiring three prior lemmas into the certificate fields.
Claim. There is a certificate asserting three facts: the determinant of the $(c,\hbar,G)$ dimension matrix is nonzero; whenever a monomial $c^a \hbar^b G^d$ is dimensionless one has $a=b=d=0$; and the SI tick-square calibration sends every positive dimensional anchor to a positive scale and is injective on anchors.
background
The module draws the honest line between Recognition Science native constants and SI units. Dimensionless identities such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$ can be forced from the framework; absolute SI values of $\hbar$ or $G$ cannot, because a dimensional bridge needs a dimensional anchor.
The three dimension vectors of $c$, $\hbar$, and $G$ form a matrix whose determinant is nonzero, so they are linearly independent over $\mathbb{Z}$. Consequently the only integer exponents making $c^a\hbar^b G^d$ dimensionless are $a=b=d=0$. The SI bridge is formalized as a map from a positive anchor (here written as a $G$-input) to a calibrated tick-square scale: that map is strictly positive on positive inputs and injective.
Upstream, the determinant claim is a one-line norm_num after unfolding the matrix determinant; the monomial claim solves the resulting linear system; the calibration claim packages positivity and injectivity of the tick-square map. The positive half (one anchor suffices and uniquely determines the full bridge) lives in SIBridgeClosure, single-anchor calibration, and the first-principles-to-SI capstone, not here.
proof idea
Term-mode inhabitant of the certificate structure. The three fields are filled by direct appeal to prior theorems: nonzero determinant of the $(c,\hbar,G)$ dimension matrix; the lemma that any dimensionless monomial forces all three exponents to zero (applied as a function on the hypothesis); and the lemma that the SI bridge is a calibration (positive on positive anchors and injective). No extra algebra is done at this site.
why it matters
Records the negative half of the dimensional story: an anchor is required, and SI conversion is calibration rather than prediction. That matches the module thesis and the framework stance that native constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ in RS units) are first-principles only up to the dimensional boundary.
No downstream consumers are wired yet in the graph. The certificate is the packaged audit point for anyone connecting T0–T8 native identities to SI output: together with the positive half (unique tick factor $a_T=\sqrt{\pi},\tau_{\mathrm{Planck}}$, single-anchor external calibration, and the first-principles-to-SI capstone with mass audit at zero hypothesis/open/external), it states that exactly one dimensional anchor determines the bridge. It does not itself compute masses or close the alpha band; it polices the boundary those results cross.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.