LedgerAlgebra
plain-language theorem explainer
LedgerAlgebra packages the transaction and ledger types with their balancing axioms and a double-entry instance into one bundle. Algebraists working on conservation in recognition models cite it when they need the basic ledger closed under addition and negation. The declaration is a direct structure definition that pulls the balancing predicates straight from the Transaction and Ledger siblings.
Claim. A structure consisting of a transaction type, a ledger type, the property that every transaction $t$ satisfies $t.debit + t.credit = 0$, the property that every ledger $L$ has net zero, and an instance of double-entry bookkeeping.
background
The module sets the ledger as the core accounting structure that enforces conservation through double-entry bookkeeping. Every transaction carries a debit and credit that must sum to zero; every ledger maintains global net zero. Transaction is the sibling structure whose balanced field supplies the debit-plus-credit axiom. Upstream LedgerForcing.balanced states that a ledger is balanced precisely when its event list is balanced, supplying the global_balance used in the ledger field.
proof idea
Structure definition that directly assigns the transaction and ledger fields to their sibling types and installs the balancing predicates by referencing the balanced field of Transaction and the global_balance field of Ledger, together with the double_entry_exists instance.
why it matters
LedgerAlgebra is the parent structure for the ledger_algebra_certificate theorem, which lists the abelian-group, conjugation-involution, and 8-window neutrality properties. It also feeds the Cycle structure and the potential_implies_exact theorem in the Algebra.LedgerAlgebra module. The declaration supplies the concrete accounting object whose closure instances become the conservation laws (energy, charge, momentum) required by the RRF foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.