G
plain-language theorem explainer
Defines Newton's gravitational constant at the CODATA 2018 SI value 6.67430×10⁻¹¹ m³ kg⁻¹ s⁻². Empiricists and report writers cite it for numeric SI comparisons only. It is a bare numeric abbreviation, intentionally kept outside the certified Recognition Science import closure.
Claim. Let $G_{\mathrm{CODATA}} := 6.67430 \times 10^{-11}$ (SI units, CODATA 2018). This is the empirical Newton constant used only for numeric SI comparisons, not the RS-native gravitational coupling.
background
The Codata module holds three quarantined SI reference numbers: the speed of light, reduced Planck's constant, and Newton's $G$. They are empirical inputs for reports and unit conversion checks. The module doc states they must stay off the certified certificate chain; any use requires an explicit import.
Recognition Science also defines an RS-native gravitational coupling $G = \lambda_{\mathrm{rec}}^2 c^3 / (\pi \hbar)$ via the recognition/Planck bridge. That object is a derived projection, not a fit to the SI digit string. Converting between the two needs the dimensional SI bridge elsewhere in the library.
Name collisions exist: a log-reparametrization $G_F(t) = F(e^t)$ appears in the cost functional-equation layer, and the inflaton potential $G(t) = \cosh t - 1 = J(e^t)$ is the J-cost in log coordinates. Those are unrelated to this CODATA literal.
proof idea
No proof. One-line noncomputable definition binding the real constant to the CODATA 2018 decimal $6.67430 \times 10^{-11}$, marked @[simp] for normalization in numeric goals.
why it matters
Gives a single, named SI anchor so empirical side-modules can quote Newton's constant without scattering magic numbers. It is deliberately excluded from the forcing chain (T0–T8) and from uniqueness results for the cost algebra: those theorems force $J(x) = \frac{1}{2}(x+x^{-1})-1$ and never read this digit string.
Downstream zero-parameter and mass-to-light certificates speak of derived constants and the RS-native bridge; they must not silently import this module. The open scaffolding item is a master certificate that all physical constants (including the SI image of $G$) are derived from the Meta-Principle once the SI bridge is closed. Until then, this definition remains a quarantined reference value for comparisons only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.