append
The append definition concatenates a transaction onto an existing ledger while updating the running debit and credit totals and re-establishing the global zero-balance invariant. Researchers modeling conservation laws or lattice-path charges in Recognition Science cite it when they need to extend a ledger without breaking double-entry closure. The construction is a direct structural update whose only non-trivial step is an omega invocation on the sum of the ledger's prior balance and the transaction's own balance constraint.
claimGiven a ledger $L$ whose transactions form a list and whose totals satisfy total debit plus total credit equals zero, and given a transaction $t$ with debit $d$ and credit $c$ satisfying $d + c = 0$, the appended ledger has transaction list equal to the concatenation of $L$'s list with the singleton list containing $t$, total debit equal to $L$'s total debit plus $d$, total credit equal to $L$'s total credit plus $c$, and global balance equal to zero.
background
A Ledger is a structure containing a list of Transactions together with running totals for debit and credit and a proof that those totals sum to zero. A Transaction is a pair of integers (debit, credit) equipped with a proof that their sum is zero; this encodes the double-entry rule that every entry has an equal and opposite counterpart. The module states that every conservation law in physics is realized as an instance of ledger closure, so the append operation is the basic mechanism that extends a conserved quantity while preserving the zero-net invariant.
proof idea
The definition is a one-line wrapper that builds a new Ledger record by list concatenation on the transaction field, integer addition on the two total fields, and a local proof that the new global balance holds. The proof extracts the balance hypothesis from the input ledger, extracts the balance hypothesis from the input transaction, and applies the omega tactic to their sum.
why it matters in Recognition Science
This definition supplies the concatenation primitive used by the winding-number theorems in WindingCharges: insert_cancelling_preserves_winding, remove_cancelling_preserves_winding, and winding_additive all rely on it to show that charges remain additive and topologically protected under path extension. It therefore sits at the base of the F-013 certificate that derives integer charge quantization and conservation from lattice-path winding numbers. The construction directly implements the conservation-law requirement stated in the module documentation.
scope and limits
- Does not accept or produce real-valued amounts; all quantities remain integers.
- Does not verify semantic correctness of a transaction beyond its internal debit-credit balance.
- Does not reorder or deduplicate transactions; order is strictly preserved by concatenation.
- Does not model external constraints such as time stamps or multi-ledger consistency.
formal statement (Lean)
96def append (L : Ledger) (t : Transaction) : Ledger := {
proof body
Definition body.
97 transactions := L.transactions ++ [t],
98 total_debit := L.total_debit + t.debit,
99 total_credit := L.total_credit + t.credit,
100 global_balance := by
101 have hL := L.global_balance
102 have ht := t.balanced
103 omega
104}
105
106/-- The net balance of a ledger (should always be 0). -/