G_SI_pos
plain-language theorem explainer
G_SI_pos asserts positivity of the CODATA gravitational constant used as an external anchor. Researchers matching Recognition Science outputs to SI measurements cite it to confirm the sign of the input value before any comparison. The proof is a direct norm_num reduction on the explicit decimal definition of G_SI.
Claim. $0 < G$ where $G = 6.67430(15) × 10^{-11}$ m³ kg⁻¹ s⁻² is the CODATA 2022 measured gravitational constant.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data entering Recognition Science. Its policy requires that the cost-first core never import it, preserving a mechanical separation between pure RCL derivations and external CODATA values. G_SI is defined here as the noncomputable real 6.67430e-11 with an accompanying uncertainty annotation.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic directly to the definition of G_SI, confirming the numerical constant satisfies the strict inequality.
why it matters
This lemma supplies a basic sign check on the gravitational constant anchor so that downstream constant comparisons remain well-defined. It fills the role of an external calibration seam without touching the RCL primitive or the phi-ladder mass formulas. The module isolates CODATA 2022 data to keep the core derivation free of measured inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.