G_SI
plain-language theorem explainer
Newton's gravitational constant in SI units, fixed at the CODATA 2018 value 6.67430e-11 m^3 kg^-1 s^-2. After the 2019 SI redefinition this is the sole remaining dimensional measurement that anchors the RS-to-SI bridge. Downstream uniqueness theorems for the tick, voxel, and coherence-mass factors cite it as the G-constraint input. Bare numeric definition, not a derived claim.
Claim. Let $G_{\mathrm{SI}} = 6.67430 \times 10^{-11}$ be Newton's gravitational constant in SI units (CODATA 2018 recommended value), with dimensions $\mathrm{m}^3\,\mathrm{kg}^{-1}\,\mathrm{s}^{-2}$.
background
The SI Bridge Closure module formalises the unique calibration map from Recognition Science native units to SI. In RS-native units the framework predicts $c_{\mathrm{RS}} = 1$, $\hbar_{\mathrm{RS}} = \varphi^{-5}$, and $G_{\mathrm{RS}} = \varphi^5/\pi$, together with the recognition/Planck bridge identity $G\cdot\pi\cdot\hbar = \lambda_{\mathrm{rec}}^2\cdot c^3$ at $\lambda_{\mathrm{rec}} = \ell_0 = 1$. Three positive conversion factors $a_T$ (sec/tick), $a_L$ (m/voxel), $a_M$ (kg/cohmass) match these against SI values via the c-, $\hbar$-, and G-constraints.
Under SI-2019 conventions, $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact definitions. The gravitational constant remains a measured CODATA input and is the single dimensional anchor for this bridge. The module proves uniqueness of the calibration once that anchor is supplied; it does not predict the SI value of $G$.
Sibling external-anchor definitions elsewhere record the same CODATA figure (with uncertainty notes) for gravity and constants modules.
proof idea
Bare numeric definition: the real is set equal to the CODATA 2018 recommended value $6.67430 \times 10^{-11}$. No proof obligations, tactics, or upstream lemmas.
why it matters
Supplies the measured side of the G-constraint $G_{\mathrm{SI}} = G_{\mathrm{RS}} \cdot a_L^3/(a_M \cdot a_T^2)$. That constraint, with the c- and $\hbar$-constraints and the native identity $\hbar_{\mathrm{RS}}\cdot G_{\mathrm{RS}} = 1/\pi$, yields the main algebraic identity $a_T^2 = \pi \cdot \hbar_{\mathrm{SI}} \cdot G_{\mathrm{SI}} / c_{\mathrm{SI}}^5$, i.e. $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$. Downstream consumers include positivity of this constant, the helper ratios $a_M a_T$ and $a_T/a_M$, and the closed-form tick conversion. In RS-native units $G = \varphi^5/\pi$ (primer constants); this SI figure is the external measurement that closes the dimensional bridge without predicting $G$ itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.