SpatialLedger
plain-language theorem explainer
A spatial ledger packages local transaction density as a non-negative real together with an integer charge fixed at zero. Gravity modelers in the Recognition Science program cite the structure when identifying mass with ledger density in the RRF foundation. The definition is introduced as a plain four-field record whose non-negativity and balance constraints are stated directly.
Claim. A spatial ledger is a tuple consisting of a density $d$ (real number of transactions per unit volume) satisfying $dgeq 0$, an integer charge $q$, and the constraint $q=0$.
background
The RRF module presents gravity as the geometric manifestation of ledger constraint density, with the explicit mapping mass equals ledger density and curvature equals constraint pressure. A ledger is balanced when its event list satisfies the balance condition from the LedgerForcing definition. The SpatialLedger structure supplies the basic object that carries density, its non-negativity witness, charge, and the zero-charge balance constraint for all subsequent gravity constructions in the file.
proof idea
The declaration is a structure definition that directly assembles the four fields density, density_nonneg, charge, and balanced. No lemmas or tactics are invoked; the record is formed by explicit field assignment.
why it matters
SpatialLedger supplies the data type underlying the gravity-ledger correspondence and the identification massFromSpatialLedger L = L.density. It is referenced by GravityLedgerCorrespondence, ledger_equals_newton, ledgerGravity, and massiveLedger. The structure realizes the module claim that gravity is collective strain from simultaneous ledger balancing and connects to the broader Recognition Science forcing chain through the ledger-balance hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.