G_codata
plain-language theorem explainer
G_codata supplies the CODATA numerical value for Newton's gravitational constant as the experimental anchor in the constants derivation module. Researchers verifying that the Recognition Science expression for G matches measured data would cite this definition. It is introduced as a direct real-number assignment with no computation or lemmas.
Claim. The CODATA reference value of Newton's gravitational constant is defined as $6.67430 times 10^{-11}$.
background
The Constants.Derivation module anchors physical constants to CODATA reference values while deriving them from Recognition Science primitives. The supplied values are $c = 299792458$ m/s, $hbar = 1.054571817 times 10^{-34}$ J s, and $G = 6.67430 times 10^{-11}$ m$^3$ kg$^{-1}$ s$^{-2}$. This definition provides the measured input for relations that connect $G$, $hbar$, and $c$ through the Recognition Composition Law and the forcing chain.
proof idea
The declaration is a direct numeric definition with no lemmas or tactics applied.
why it matters
This definition anchors the derived gravitational constant to experimental data and enables the theorem G_relation_satisfied that proves equality between the derived and CODATA values. It supports the positivity and non-zero lemmas used throughout the module and connects to the framework expression $G = phi^5 / pi$ in RS-native units. The value closes the loop from the eight-tick octave and phi-ladder back to laboratory measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.