massFromLedger
plain-language theorem explainer
The definition computes mass as the product of a ledger density value and a supplied volume. It would be cited in RRF derivations that map transaction counts per unit volume to gravitational mass. The implementation is a direct field projection followed by multiplication.
Claim. Given a ledger density structure $L$ whose density field satisfies $0 ≤ ρ_L$ and a real volume $V$, the associated mass is $m = ρ_L · V$.
background
The RRF Foundation module treats the ledger as the fundamental accounting structure that enforces conservation via double-entry bookkeeping, requiring debit plus credit to sum to zero for every transaction. LedgerDensity is the structure holding a real density field (transactions per unit volume) together with a non-negativity proof. The definition supplies mass by scaling this density by the given volume, consistent with upstream volume definitions that count vertices in a finite set and density constructions appearing in related physics modules.
proof idea
The definition is a one-line wrapper that extracts the density component of the LedgerDensity structure and multiplies it by the volume argument.
why it matters
This definition supplies the direct gravity mapping from ledger density to mass inside the RRF ledger algebra. It sits at the base of curvature interpretations that connect transaction accounting to physical mass, aligning with the Recognition Science derivation of quantities from ledger closure. No downstream theorems are recorded, leaving open its integration with the phi-ladder mass formulas and constants such as G = phi^5 / pi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.