newtonGravity
plain-language theorem explainer
The declaration defines the Newtonian gravitational force as G times mass over radius squared using a placeholder constant. Researchers equating ledger-based curvature models to classical gravity would cite it when verifying that constraint density reproduces the inverse-square law. It is implemented as a direct noncomputable definition that multiplies the constant by the supplied mass and divides by the squared distance.
Claim. The Newtonian gravitational force is given by $F = G M / r^2$, where $G = 6.674 times 10^{-11}$ is the placeholder value for Newton's constant.
background
In the RRF module gravity is the geometric manifestation of ledger constraint density, with mass identified as the number of transactions per volume and curvature identified as the tightness of the ledger. The definition supplies the classical target expression to which ledger-based computations are compared. It rests on the RecognitionStructure M (encoding a universe set U together with a recognition function R) and its Cycle3 specialization to a three-element cycle, plus the sibling constant G_Newton.
proof idea
The definition is a direct abbreviation that multiplies the placeholder G_Newton by the mass parameter and divides by the square of the radius parameter.
why it matters
This definition anchors the classical Newtonian limit inside the ledger-curvature model. It is invoked by the downstream theorem ledger_equals_newton, which states that ledgerGravity L r equals newtonGravity (massFromSpatialLedger L) r by reflexivity. The surrounding module claims that gravity is the collective strain of particles balancing their ledgers simultaneously rather than an independent force, thereby filling the step from ledger density to observable inverse-square behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.