G_pos
plain-language theorem explainer
The lemma asserts positivity of the CODATA gravitational constant G = 6.67430e-11. Bridge constructions in DataCore cite it to satisfy the Physical assumptions structure when proving positivity of lambda_rec. The proof is a one-line reduction that unfolds the numeric definition and applies norm_num.
Claim. $0 < G$ where $G = 6.67430e-11$ is the CODATA 2018 value of Newton's gravitational constant.
background
The Codata module quarantines empirical SI constants (c, hbar, G) from the certified Recognition Science chain so that the main certificate does not depend on numeric values. G is defined here as the literal 6.67430e-11. The lemma supplies the positivity fact required by the Physical structure in Bridge.DataCore, which packages c_pos, hbar_pos and G_pos to support analytic lemmas such as lambda_rec_pos.
proof idea
One-line wrapper that unfolds G to its numeric literal and invokes norm_num.
why it matters
It supplies the G_pos field demanded by the Physical structure, which is invoked by lambda_rec_pos and lambda_rec_dimensionless_id_physical in Bridge.DataCore. The module doc explicitly quarantines these constants to keep empirical numbers out of the certified surface; the RS-native G_pos in ConstantDerivations instead derives positivity from the expression lambda_rec^2 c^3 / (pi hbar). No open question is resolved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.