massFromSpatialLedger
plain-language theorem explainer
Mass is identified with the transaction density recorded in a local spatial ledger. Researchers deriving Newtonian gravity or curvature from ledger constraints cite this identification to equate mass to density before applying the ledgerGravity construction. The definition is a direct one-line projection of the density field from the SpatialLedger structure.
Claim. For a spatial ledger $L$ with non-negative density $d$, integer charge, and local balance constraint, the associated mass is $m(L) = d$.
background
The RRF module treats gravity as the geometric manifestation of ledger constraint density, with the explicit mapping that mass equals ledger density (transactions per unit volume) and curvature equals constraint pressure. SpatialLedger is the structure that records this local information: a real-valued density field, an integer charge, and the balance condition that charge equals zero. Upstream, Mass is simply an abbreviation for the reals, while related ledger constructions appear in SimplicialLedger and Cycle3 modules.
proof idea
One-line definition that projects the density component directly from the SpatialLedger structure.
why it matters
This definition supplies the mass_is_density field inside the GravityLedgerCorrespondence structure and is invoked by ledger_equals_newton and ledgerGravity to recover the Newtonian inverse-square law by construction. It realizes the module's central claim that gravity is collective strain of particles balancing ledgers simultaneously, linking to the Recognition Science identification of mass with phi-ladder densities in native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.