ledger_equals_newton
plain-language theorem explainer
The declaration establishes that gravity computed from a spatial ledger at distance r matches the Newtonian formula once the ledger mass is extracted. Researchers modeling emergent gravity from discrete transaction balances would cite this equivalence. The proof is a one-line reflexivity that holds because the two sides are constructed to coincide by definition.
Claim. Let $L$ be a spatial ledger and let $r$ be a nonzero real number. The gravitational acceleration derived from the ledger at distance $r$ equals the Newtonian gravitational acceleration computed from the mass extracted from $L$ at the same distance.
background
In the RRF setting gravity is the geometric manifestation of ledger constraint density, with mass identified as ledger density (transactions per unit volume) and curvature identified as constraint pressure. A SpatialLedger is a structure carrying a non-negative real density, an integer charge required to be zero, and the corresponding balance constraint. The module imports define active edge count per tick as the constant 1 and supply simplicial ledger bridges that identify discrete edge lengths with continuum Laplacian actions.
proof idea
The proof is a one-line reflexivity that applies the definitional equality between ledgerGravity and newtonGravity once massFromSpatialLedger has been substituted.
why it matters
The result anchors the claim that gravity is ledger curvature rather than a primitive force. It supplies the direct link between the spatial ledger structure and classical Newtonian gravity inside the RRF foundation, supporting the mapping from transaction density to mass and from constraint pressure to curvature. The equivalence closes one step in the chain from discrete ledgers to continuum gravity without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.