G_Newton
plain-language theorem explainer
This definition supplies the numerical placeholder 6.674e-11 for Newton's gravitational constant in RRF ledger calculations. Researchers bridging Recognition Science derivations to classical gravity expressions cite it when constructing Newtonian forms from ledger density. The definition is a direct constant assignment with no further reduction steps.
Claim. Newton's gravitational constant is assigned the numerical value $6.674 times 10^{-11}$ in SI units as a placeholder.
background
The RRF Foundation module treats gravity as the geometric manifestation of ledger constraint density. Mass equals ledger density (transactions per volume) and curvature equals constraint pressure, so gravity appears as collective strain when particles balance ledgers simultaneously rather than as an independent force. Upstream, Constants.G derives the constant from first principles as $lambda_rec^2 c^3 / (pi hbar)$, while Constants.Codata.G records the matching CODATA numerical value 6.67430e-11.
proof idea
The definition is a direct noncomputable assignment of the floating-point constant 6.674e-11 with no lemmas or tactics applied.
why it matters
This supplies the numerical anchor for the downstream definitions ledgerGravity, newtonGravity, and schwarzschildRadius. It provides the interface between the Recognition Science derivation of G (via the phi-ladder and RCL, with native form phi^5 / pi) and observed Newtonian behavior, consistent with the module claim that gravity is ledger curvature. It leaves open the exact scaling from RS-native units to SI values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.