pith. machine review for the scientific record. sign in
def

G_SI

definition
show as:
module
IndisputableMonolith.Constants.ExternalAnchors
domain
Constants
line
98 · github
papers citing
none yet

plain-language theorem explainer

G_SI supplies the CODATA 2022 measured value of Newton's gravitational constant as 6.67430 × 10^{-11} m³ kg^{-1} s^{-2}. Researchers calibrating Recognition Science native predictions against laboratory data cite this external anchor. It is realized as a direct noncomputable definition carrying the numerical assignment together with the simp attribute.

Claim. $G = 6.67430 × 10^{-11} m³ kg^{-1} s^{-2}$ (CODATA 2022)

background

The ExternalAnchors module is the single quarantined location for all empirical calibration data that enters Recognition Science. Its policy keeps the cost-first core, which derives everything from the Recognition Composition Law, free of external imports; any module that brings in ExternalAnchors explicitly signals use of measured anchors, and all entries carry the external_anchor attribute.

proof idea

one-line wrapper that assigns the numerical value 6.67430e-11 directly to the real number G_SI.

why it matters

This anchor populates the AbsolutePack structure for SI reference displays and supports the G_SI_pos positivity lemma. It closes the calibration path from the RS-native expression G = phi^5 / pi (derived in the T0-T8 forcing chain) to measured values, enabling quantitative checks while preserving the independence of the pure RCL core.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.