G
plain-language theorem explainer
Empirical gravitational constant from CODATA 2018. Researchers comparing Recognition Science derivations to measured values cite this quarantined constant for numeric checks. It is a direct numeric assignment with no internal derivation.
Claim. The gravitational constant equals $6.67430 times 10^{-11}$ in SI units.
background
The module quarantines empirical SI/CODATA constants from the certified surface so the top-level certificate chain does not depend on numeric values. This G supplies the measured value, distinct from the first-principles form $G = lambda_rec^2 c^3 / (pi hbar)$ in Constants.G. The module doc states these constants are intentionally isolated for optional empirical reports.
proof idea
One-line definition that assigns the CODATA 2018 numeric value directly.
why it matters
Supplies the empirical anchor for comparisons in CostAlgebra theorems (cost_algebra_unique, J_defect_form) and Astrophysics modules (H_RSZeroParameterStatus, ml_zero_parameter_certificate). It supports checks against the derived constants from the forcing chain (T5 J-uniqueness, T8 D=3) while remaining outside the certified import closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.