add_balanced
plain-language theorem explainer
The add_balanced theorem establishes that the sum of any two transactions remains balanced, with the combined debit and credit summing to zero. Researchers modeling conservation via double-entry structures in Recognition Science cite it when composing ledger operations. The proof is a direct term projection of the balanced field from the add result.
Claim. For any transactions $t_1$ and $t_2$, each satisfying debit + credit = 0 by structure, the sum transaction satisfies debit(add $t_1$ $t_2$) + credit(add $t_1$ $t_2$) = 0.
background
Transaction is a structure with integer debit (outflow), integer credit (inflow), and an attached proof that debit + credit = 0. This encodes the double-entry rule at the level of a single event. The module treats a Ledger as a list of such transactions whose global sum enforces conservation for any physical quantity.
proof idea
The proof is a one-line term wrapper that applies the balanced field carried by the result of the add operation on the two input transactions.
why it matters
The result ensures addition preserves the zero-balance invariant, supporting construction of closed ledgers that instantiate conservation laws. It sits inside the RRF ledger algebra and aligns with the framework's view that every conservation law is an instance of ledger closure. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.