ledgerGravity
plain-language theorem explainer
The ledger-based gravity definition computes the field strength at distance r from a spatial ledger point by scaling the ledger-derived mass with the placeholder Newtonian constant and dividing by r squared. Researchers embedding classical gravity into ledger-constraint models would cite this as the direct mapping from Recognition density to Newtonian force. It is realized as a direct algebraic expression with no additional steps.
Claim. For a spatial ledger $L$ with density $d$, the gravitational field at distance $r$ is $G_N d / r^2$, where $G_N$ is the placeholder Newtonian constant and mass is identified with ledger density.
background
In the RRF Foundation module gravity is presented as the geometric manifestation of ledger constraint density. A SpatialLedger records transaction density (transactions per unit volume) at a point, required to be non-negative with zero net charge. The massFromSpatialLedger function identifies mass directly with this density. Newton's constant is supplied as the placeholder value 6.674e-11. This construction sits inside the Recognition framework where ledgers track debit and credit balances.
proof idea
The definition is a one-line wrapper that applies massFromSpatialLedger to extract density as mass, multiplies by G_Newton, and divides by r squared.
why it matters
This definition supplies the explicit form of gravity used by the downstream theorem ledger_equals_newton, which establishes equality with classical Newtonian gravity by construction. It realizes the module claim that gravity is the collective strain of particles balancing their ledgers simultaneously and links to the Recognition identification of mass with ledger density. It leaves open the derivation of the numerical value of G from phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.