zero
plain-language theorem explainer
The zero transaction is the trivial balanced entry obtained by applying fromAmount to the integer zero. Ledger algebra users cite this as the additive identity for transaction composition. The definition is a direct one-line wrapper around fromAmount.
Claim. The zero transaction $T_0$ is the balanced transaction with debit amount $0$ and credit amount $0$, constructed by applying fromAmount to the integer $0$.
background
In the RRF foundation the ledger models double-entry bookkeeping. The Transaction structure consists of an integer debit (outflow), an integer credit (inflow), and a proof that debit + credit = 0. The fromAmount function creates such a transaction from a single integer amount by setting debit to the amount and credit to its negation, with the balance proved by omega.
proof idea
The definition is a one-line wrapper that applies fromAmount to the integer 0.
why it matters
This definition supplies the zero element for the additive structure of transactions. It supports the conservation laws in the module, where each conservation law (energy, charge, momentum) is realized as ledger closure. The construction anchors the double-entry constraint debit + credit = 0 that the ledger algebra enforces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.