G_ne_zero
plain-language theorem explainer
The lemma establishes that the CODATA 2018 numerical value of Newton's gravitational constant is nonzero. Researchers importing the quarantined empirical constants module cite it to license divisions or positivity arguments involving G. The proof is a one-line term that applies ne_of_gt directly to the positivity lemma G_pos.
Claim. Let $G$ denote the CODATA 2018 numerical value of Newton's gravitational constant. Then $G$ is nonzero.
background
The declaration sits inside the Codata module, which isolates empirical SI/CODATA constants from the certified Recognition Science surface. The module defines $G$ as the literal value 6.67430e-11 and proves the companion positivity statement $0 < G$ by unfolding the definition and applying norm_num. Upstream results supply the RS-native expression for $G$ in the main Constants module, given by $G = (lambda_rec^2) c^3 / (pi hbar)$, together with its own positivity proof obtained by applying div_pos to the positivity of lambda_rec and c.
proof idea
The proof is a direct term ne_of_gt G_pos. It invokes the standard fact that every positive real number is nonzero and feeds it the already-established positivity lemma for the CODATA value.
why it matters
The lemma supplies a minimal guard for numeric work inside the quarantined constants module, mirroring the positivity result already proved for the derived RS-native $G$. No downstream uses are recorded, consistent with the explicit quarantine that prevents the top-level certificate chain from depending on these empirical numbers. It therefore touches the framework's separation between the phi-ladder derivations and the CODATA reference values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.