curvatureFromLedger
plain-language theorem explainer
CurvatureFromLedger supplies the mapping from ledger density to a real-valued curvature inside the RRF ledger algebra. Researchers deriving gravitational effects from transaction conservation would cite this when converting accounting structures into spacetime curvature. The definition is a direct field projection from the LedgerDensity record, presented as a placeholder for a fuller functional form.
Claim. For a ledger density structure $L$ with non-negative real component $ρ$, the induced curvature is defined by $κ(L) := ρ$.
background
The RRF Foundation module treats the ledger as the core accounting structure that enforces conservation. Every transaction satisfies the double-entry rule that debit plus credit equals zero, so each conservation law for energy, charge or momentum appears as an instance of ledger closure. LedgerDensity is the structure that records the number of transactions per unit volume together with the non-negativity constraint $0 ≤ ρ$.
proof idea
The definition is a one-line projection that returns the density field of the supplied LedgerDensity structure.
why it matters
This definition supplies the gravity-mapping interface that converts ledger density into curvature, thereby linking the double-entry conservation principle to geometric quantities. It sits at the foundation of the RRF ledger algebra and prepares the ground for later derivations that connect transaction counts to spatial structure, although no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.