Transaction
plain-language theorem explainer
Transaction encodes a balanced debit-credit pair as the atomic unit of the RRF ledger. Researchers constructing conservation laws for energy or charge cite this structure when assembling additive ledgers from double-entry rules. The definition is a direct structure whose third field is the integer equation debit + credit = 0.
Claim. A transaction is a pair of integers $(d, c)$ satisfying $d + c = 0$.
background
The RRF Foundation module treats the ledger as the core accounting structure that enforces conservation through double-entry bookkeeping. Every transaction records an outflow (debit) and inflow (credit) whose sum must vanish, so that each conservation law (energy, charge, momentum) appears as an instance of ledger closure. The upstream balanced predicate from LedgerForcing states that a ledger is balanced precisely when its event list satisfies the same sum-zero condition, while the from theorem in PrimitiveDistinction extracts four structural conditions plus three definitional facts from seven independent axioms.
proof idea
The declaration is a structure definition whose fields are debit : ℤ, credit : ℤ and the field balanced : debit + credit = 0. No tactics or lemmas are invoked; the balance constraint is simply part of the type.
why it matters
Transaction supplies the atomic building block for the Ledger structure and its operations add, append and fromAmount, all of which preserve the balance field. It therefore sits at the base of the conservation-law machinery that Recognition Science uses to derive physical quantities from the forcing chain (T0-T8) and the Recognition Composition Law. The definition directly supports downstream constructions such as SpatialLedger in the Gravity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.