G_codata_ne_zero
plain-language theorem explainer
The lemma asserts that the CODATA numerical value for Newton's gravitational constant is nonzero. Researchers verifying Planck-scale identities in Recognition Science cite it to license divisions by G inside hbar derivations. The proof is a one-line term that applies ne_of_gt directly to the positivity lemma for the same constant.
Claim. Let $G_0 = 6.67430e-11$. Then $G_0 ≠ 0$.
background
Constants.Derivation records the three CODATA anchors as plain real numbers: c, ℏ, and G. G_codata is the direct assignment 6.67430e-11. Its positivity is recorded separately by unfolding the definition and applying norm_num. Time is the abbreviation for ℝ used throughout the dimensioned constants.
proof idea
The proof is a one-line term wrapper: ne_of_gt applied to G_codata_pos. No further tactics or reductions are required.
why it matters
The lemma is invoked inside planck_relation_satisfied to obtain the hypothesis G_codata ≠ 0 before rewriting the derived hbar expression. It therefore closes the only division-by-zero risk in the constant-matching theorem. Within the Recognition framework it anchors the numerical value of G that is later identified with phi^5 / pi in native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.