empty
plain-language theorem explainer
The empty ledger is the zero element of the RRF ledger algebra, consisting of an empty transaction list with zero debit and credit sums. Researchers in ledger-based conservation laws and complexity theory cite it as the base case for inductive arguments on balanced structures. The definition constructs the Ledger record directly and discharges the balance constraint via the omega tactic.
Claim. The empty ledger is the structure with transactions $= []$, total debit $= 0$, total credit $= 0$, and global balance satisfying $0 + 0 = 0$.
background
In the RRF foundation the ledger is the core accounting structure that enforces conservation via double-entry bookkeeping. Every transaction records a debit and a credit whose sum is zero; the global balance condition total_debit + total_credit = 0 ensures closure for any conserved quantity. The Ledger structure packages a list of transactions with their summed debit and credit fields together with an explicit proof of the balance equation. The empty ledger supplies the initial object with no entries. Upstream results include the singleton ledger construction that extends this base case to a single transaction.
proof idea
This is a direct definition that builds the Ledger record literal. The transactions field is the empty list, the totals are set to zero, and the global_balance field is discharged by the omega tactic on the trivial arithmetic identity 0 + 0 = 0.
why it matters
This definition supplies the base case for ledger algebra and appears in more than forty downstream results, including the IsBalanced predicate and the P versus NP resolution through recognition scales. It anchors the conservation laws required by the RRF framework and supports theorems on natural properties in complexity by providing the trivial balanced case. It is the starting point for inductive arguments that reach the forcing chain and recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.