pith. machine review for the scientific record. sign in
def definition def or abbrev high

G_SI

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  98@[simp]
  99noncomputable def G_SI : ℝ := 6.67430e-11

proof body

Definition body.

 100
 101/-- **EXTERNAL ANCHOR**: Gravitational constant uncertainty (1σ). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.