G
plain-language theorem explainer
CODATA 2018 Newton's gravitational constant is fixed as the SI real 6.67430e-11. Cite it only for explicit SI numeric comparisons or empirical reports against RS predictions. The body is a bare numeric literal with the simp attribute; no derivation is claimed.
Claim. Newton's gravitational constant in SI units is the real number $G = 6.67430 \times 10^{-11}$ (CODATA 2018).
background
This module holds quarantined empirical SI/CODATA anchors: speed of light, reduced Planck constant, and Newton's $G$. They are deliberately kept off the certified import-closure so the top-level certificate chain never depends on measured SI digits.
Do not confuse this literal with the RS-native gravitational coupling in Constants, which is the bridge projection $G = \lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ and is not a prediction of the SI value. Two other namesakes exist: the log reparametrization $G_F(t)=F(e^t)$ in the cost functional-equation layer, and the inflaton potential $G(t)=\cosh t-1=J(e^t)$ from T5's $J$.
SI conversion of the RS-native coupling requires the dimensional bridge in Foundation/SIBridgeClosure; this definition supplies only the external CODATA target for such comparisons.
proof idea
Definition, not a proof: a noncomputable def assigning the CODATA 2018 decimal literal 6.67430e-11 in ℝ, marked @[simp] for normalization in numeric goals. No lemmas are applied.
why it matters
Gives a single named SI anchor so astrophysics and constants reports can compare RS outputs to laboratory $G$ without smuggling measured digits into the forcing chain (T5 J-uniqueness, RCL, phi, eight-tick, $D=3$). The module doc forbids the certificate surface from importing it; consumers must import Constants.Codata explicitly.
Downstream zero-parameter and mass-to-light certificates speak of deriving $G$ in RS-native form, not this CODATA literal. The RS-native projection and the SI bridge remain the predictive path; this symbol is the empirical yardstick those bridges are checked against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.