LedgerDensity
plain-language theorem explainer
LedgerDensity introduces a non-negative real scalar for transaction count per unit volume inside the RRF ledger algebra. MassFromLedger and curvatureFromLedger cite it to convert accounting data into mass and curvature values. The declaration is realized as a bare structure with a single non-negativity field.
Claim. A ledger density is a real number $d$ satisfying $d ≥ 0$, where $d$ counts transactions per unit volume.
background
The module sets the ledger as the fundamental accounting object that enforces conservation via double-entry rules: every transaction records equal debit and credit so that total debit plus total credit equals zero. The sibling Ledger structure packages a list of transactions together with explicit total_debit and total_credit sums that satisfy the global balance equation. Upstream structures supply the J-cost calibration from PhiForcingDerived and the tiered nuclear densities from NucleosynthesisTiers, which locate physical quantities on discrete φ-ladders.
proof idea
The declaration is a structure definition that directly introduces the two fields density : ℝ and nonneg : 0 ≤ density.
why it matters
LedgerDensity supplies the density argument to massFromLedger (density times volume) and to curvatureFromLedger (the gravity mapping). It therefore bridges the abstract ledger algebra to the Recognition Science mass formula that places masses on the φ-ladder and to the conservation laws enforced by ledger closure. The definition remains open on the concrete map from a balanced Ledger to a numerical density value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.