Ledger
plain-language theorem explainer
A ledger is a finite list of internally balanced transactions whose aggregate debit and credit sums cancel. Modelers of conservation laws in the Recognition framework cite this structure when encoding double-entry rules for quantities such as energy or charge. The declaration is a plain structure definition that computes the two totals by list summation and asserts the single global-balance equation.
Claim. A ledger consists of a list of transactions $T_i$, each satisfying debit$_i$ + credit$_i$ = 0, together with the derived totals $D = $ sum of all debits and $C = $ sum of all credits, subject to the constraint $D + C = 0$.
background
The RRF module presents the ledger as the core accounting structure that enforces conservation. It realizes double-entry bookkeeping in which every transaction records a debit and a credit that cancel, so that conservation laws for energy, charge, momentum and similar quantities appear as instances of ledger closure. A Transaction is the elementary record carrying an integer debit, an integer credit, and the local balance equation debit + credit = 0. The Ledger aggregates a list of such records, obtains total_debit and total_credit by mapping and summation, and requires their sum to vanish. Upstream summation primitives (map from RSNative.Core and total from DiscreteVorticity and ErrorBudget) supply the list-processing operations used to define the aggregates.
proof idea
The declaration is a structure definition. It introduces the transactions field as a List Transaction, defines total_debit and total_credit by applying the map-and-sum pattern to the debit and credit projections, and adds the global_balance field as the equality total_debit + total_credit = 0.
why it matters
The structure supplies the primitive that lets every conservation law be expressed as ledger closure, the central claim of the RRF foundation module. It therefore sits at the base of any later encoding of physical balance equations. No downstream theorems are recorded, so its integration with concrete models such as discrete vorticity or Riemann error budgets remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.