fromAmount
plain-language theorem explainer
fromAmount constructs a balanced transaction by setting debit to an integer amount and credit to its negation. Ledger algebra in Recognition Science uses this to enforce zero-sum conservation in double-entry bookkeeping. The definition directly builds the Transaction record and discharges the balance condition via the omega tactic.
Claim. The map sending each integer $a$ to the transaction with debit $a$ and credit $-a$, satisfying the zero-sum constraint debit + credit = 0.
background
The RRF ledger algebra models conservation through double-entry bookkeeping. Every transaction consists of a debit and a credit that must sum to zero, as captured by the Transaction structure with fields debit : ℤ, credit : ℤ, and balanced : debit + credit = 0. This definition creates such a transaction from a single integer amount. It depends on the balanced predicate from the LedgerForcing module, which ensures the event list satisfies conservation.
proof idea
This is a direct record construction that sets debit to the input amount and credit to its negation. The balanced field is discharged by the omega tactic solving the linear equation debit + credit = 0.
why it matters
This definition supplies the basic constructor for transactions in the ledger algebra. It is used to define the zero transaction, which serves as the identity in the additive structure of transactions. In the Recognition framework, it supports the enforcement of conservation laws across physical quantities like energy and charge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.