NativeDimensionalBoundaryCert
plain-language theorem explainer
Certificate packaging the dimensional-boundary audit for Recognition Science constants: the (c, ℏ, G) dimension matrix is invertible over the integers, no nontrivial monomial of those three is dimensionless, and the SI tick-scale map from a positive G anchor is positive and injective. Cited by anyone separating first-principles native identities from SI conversion. Structure definition only; the witness instance is built by a sibling theorem.
Claim. A certificate of three properties: (i) the $3\times 3$ integer matrix whose columns are the $(L,T,M)$ dimension exponents of $c$, $\hbar$, and $G$ has nonzero determinant; (ii) whenever $c^a \hbar^b G^d$ is dimensionless (exponents $(0,0,0)$ in length, time, mass), one has $a=b=d=0$; (iii) the squared tick scale the SI bridge assigns from a positive input Newton constant $G_{\mathrm{in}}$ is always positive, and the map $G_{\mathrm{in}}\mapsto$ that scale is injective.
background
This module draws the honest line between RS-native dimensionless identities and absolute SI values. The framework forces relations such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$, but pure dimensionless data cannot fix the SI magnitude of $\hbar$ or $G$. A dimensional bridge needs one dimensional anchor.
The dimension map sends integer exponents $(a,b,d)$ of the monomial $c^a\hbar^b G^d$ to the triple $(L,T,M)$ via $c\sim L T^{-1}$, $\hbar\sim M L^2 T^{-1}$, $G\sim L^3 M^{-1} T^{-2}$. The associated $3\times 3$ matrix has columns $(1,-1,0)$, $(2,-1,1)$, $(3,-2,-1)$; its determinant is $-2$, so the three constants are dimensionally independent (they span an index-2 sublattice of $\mathbb{Z}^3$).
The calibrated squared tick is $\pi,\hbar_{\mathrm{SI}},G_{\mathrm{in}}/c_{\mathrm{SI}}^5$, the same algebraic shape as the closed SI-bridge identity $a_T=\sqrt{\pi},\tau_{\mathrm{Planck}}$, but with $G$ left free to expose anchor dependence. The positive half (one anchor suffices and uniquely determines the bridge) lives in SIBridgeClosure, SingleAnchor, and the first-principles-to-SI capstone; this module only packages the negative half.
proof idea
No proof body: this is a structure definition whose three fields are propositions. Field one asserts $\det$ of the $(c,\hbar,G)$ dimension matrix is nonzero. Field two is the kernel statement that only the zero exponent triple yields a dimensionless monomial. Field three packages positivity of the calibrated squared tick for every positive $G_{\mathrm{in}}$ together with injectivity of that map. The sibling theorem native_dimensional_boundary_cert fills the fields by citing the determinant lemma, the no-nontrivial-dimensionless-monomial lemma, and the SI-bridge-is-calibration lemma.
why it matters
Marks where first-principles RS stops and SI calibration begins. Downstream, native_dimensional_boundary_cert inhabits the structure and states that native constants are first-principles objects only up to the dimensional boundary; SI conversion is a uniquely constrained calibration once an anchor is supplied. That matches the module thesis: exactly one dimensional anchor determines the whole bridge (tick factor, meters per voxel, joules per coherence unit), as already proved positively in SIBridgeClosure and the T0–T8-plus-single-anchor mass capstone. Ties to the RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ by clarifying that those equalities are dimensionless/native, not automatic SI predictions. No open scaffold: the certificate is the packaging layer for an already-closed audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.