net
plain-language theorem explainer
Defines the net balance of a ledger as the sum of its total debit and total credit. Researchers modeling conservation laws in Recognition Science cite this when verifying zero-net properties across accounting structures. The definition is a direct extraction of the precomputed aggregate fields from the Ledger structure.
Claim. For a ledger $L$, the net balance is defined by $net(L) := d(L) + c(L)$, where $d(L)$ is the sum of all debits and $c(L)$ the sum of all credits over the transactions in $L$.
background
The RRF Foundation module presents the ledger as the core accounting structure that enforces conservation via double-entry bookkeeping. Every transaction records a debit and credit pair, and the fundamental constraint requires their totals to sum to zero. A Ledger is a structure containing a list of transactions together with precomputed total_debit and total_credit fields plus an explicit global_balance proof that their sum vanishes.
proof idea
One-line definition that directly returns the sum of the total_debit and total_credit fields stored inside the Ledger structure.
why it matters
This definition supplies the basic net-balance operation used throughout the Recognition framework to express conservation. It feeds directly into GradedLedger (inflow equals outflow at every vertex) and OctaveLoop (zero net recognition flux after eight steps). The construction aligns with the ledger-closure principle that turns every conservation law (energy, charge, momentum) into an instance of double-entry balance, supporting the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.