concat
plain-language theorem explainer
Concatenation joins two ledgers by appending transaction lists and summing their debit and credit totals while preserving the zero-balance invariant. Researchers formalizing conservation laws in the RRF ledger algebra cite this definition when composing accounting structures. The definition assembles the output record directly and applies the omega tactic to the pair of input balance hypotheses.
Claim. Let $L_1$ and $L_2$ be ledgers. Their concatenation is the ledger whose transaction list is $L_1$.transactions $++$ $L_2$.transactions, whose total debit is $L_1$.total_debit $+$ $L_2$.total_debit, whose total credit is $L_1$.total_credit $+$ $L_2$.total_credit, and whose global balance satisfies total_debit $+$ total_credit $= 0$.
background
In the RRF Foundation Ledger module the ledger is the core accounting structure that enforces conservation through double-entry bookkeeping. A ledger consists of a list of transactions together with aggregated debit and credit totals required to satisfy total_debit + total_credit = 0. Module documentation states that each conservation law (energy, charge, momentum) appears as an instance of ledger closure.
proof idea
The definition constructs the new ledger record by concatenating the transaction lists with ++ and adding the debit and credit fields with +. The global_balance field is discharged by applying omega to the two input balance equalities.
why it matters
The definition is invoked by the downstream theorem concat_preserves_balance, which confirms that the concatenated ledger maintains net zero balance. It supports the framework's identification of conservation laws with ledger instances, consistent with the double-entry constraint that debit plus credit sums to zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.