massiveLedger
plain-language theorem explainer
massiveLedger constructs a spatial ledger instance carrying positive density d as mass at a point. Researchers modeling gravity as ledger curvature in the RRF framework cite it to populate non-vacuum regions with the mass-density identification. The definition is a direct record construction that assigns density, derives non-negativity from the input inequality, and enforces zero charge with reflexivity.
Claim. For real number $d > 0$, the massive ledger is the spatial ledger with transaction density $d$, non-negative density, zero charge, and balanced constraint.
background
The RRF module treats gravity as the geometric effect of ledger constraint density, with the explicit mapping mass equals ledger density (transactions per unit volume) and curvature equals constraint pressure. The SpatialLedger structure packages a real density field, a non-negativity proof, an integer charge, and the balanced predicate requiring charge zero. This definition supplies the non-vacuum case, set against the zero-density vacuumLedger in the same file.
proof idea
The definition is a direct record literal. It sets the density field to the parameter d, obtains density_nonneg by applying le_of_lt to the positivity hypothesis, fixes charge at zero, and discharges the balanced field by reflexivity.
why it matters
It supplies the basic non-vacuum ledger object that realizes the mass-density identification central to the module claim that gravity is collective ledger strain. The construction feeds the sibling massFromSpatialLedger and curvatureFromStrain definitions, closing the local ledger-to-geometry step in the RRF foundation. It aligns with the Recognition Science T8 spatial dimension and the ledger-forcing balance axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.