G_codata_pos
plain-language theorem explainer
The lemma shows that the CODATA value assigned to Newton's gravitational constant is strictly positive. Workers constructing Planck length, mass, and time from Recognition Science constants rely on it to validate positivity in divisions and square roots. The argument is a direct numerical check after unfolding the definition.
Claim. $0 < G$ where $G = 6.67430$ e-11 denotes the CODATA gravitational constant in SI units.
background
The Constants.Derivation module introduces the CODATA reference values for c, ℏ, and G to ground subsequent derivations in Recognition Science. The gravitational constant is defined directly as the real number 6.67430e-11. This supplies the base numerical anchor used by all later positivity claims in the module.
proof idea
The proof is a one-line wrapper that unfolds the definition of the gravitational constant to expose the literal 6.67430e-11 and then invokes norm_num to discharge the inequality.
why it matters
Eight lemmas depend on this result, including the non-zero claim for G, the positivity of the inner Planck expression, and the positive Planck length, mass, and time. It supplies the base positivity for the constant derivations that feed into the Recognition Science time quantum relations. The module doc-comment frames these as CODATA anchors for the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.