massFromLedger
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.
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not incorporate phi-ladder rung adjustments or gap(Z) corrections.
- Does not enforce additional conservation laws beyond density non-negativity.
- Does not produce numerical values for physical constants or scaling factors.
formal statement (Lean)
176noncomputable def massFromLedger (L : LedgerDensity) (volume : ℝ) : ℝ :=
proof body
Definition body.
177 L.density * volume
178
179/-- Curvature from ledger density (the gravity mapping). -/