add
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not handle non-integer amounts or real-valued quantities.
- Does not define multiplication, scalar action, or other ring operations.
- Does not establish associativity, commutativity, or identity elements.
- Does not address ledgers containing more than two events at once.
formal statement (Lean)
50def add (t₁ t₂ : Transaction) : Transaction := {
proof body
Definition body.
51 debit := t₁.debit + t₂.debit,
52 credit := t₁.credit + t₂.credit,
53 balanced := by
54 have h₁ := t₁.balanced
55 have h₂ := t₂.balanced
56 omega
57}
58