add
plain-language theorem explainer
Addition on transactions sums their debit and credit fields componentwise while preserving the zero-balance constraint. A ledger theorist or conservation-law modeler would cite this when composing events that each obey double-entry rules. The definition performs direct field addition and discharges the new balance obligation via the omega tactic applied to the two input equalities.
Claim. For transactions $t_1$ and $t_2$ each satisfying debit + credit = 0, the sum transaction has debit equal to the sum of the two debits and credit equal to the sum of the two credits, which again satisfies debit + credit = 0.
background
In the RRF ledger algebra a Transaction is an integer pair (debit, credit) obeying debit + credit = 0; this encodes conservation of any quantity through double-entry bookkeeping. The module presents the ledger as the core structure that enforces such conservation laws for energy, charge, momentum and similar quantities. The upstream balanced definition states that a ledger is balanced precisely when its event list is balanced, supplying the closure property used here.
proof idea
The definition constructs the result by setting debit := t₁.debit + t₂.debit and credit := t₁.credit + t₂.credit. It then proves the balanced field by extracting the two input balance hypotheses and invoking the omega tactic, which immediately yields the required sum-zero equation.
why it matters
This supplies the additive operation on transactions, allowing composition of conservation events while maintaining ledger closure. It forms part of the algebraic foundation for treating all physical conservation laws as instances of balanced ledgers in the Recognition Science framework. No downstream uses are recorded, so the declaration functions as a primitive building block rather than a derived lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.