singleton
plain-language theorem explainer
Singleton builds the minimal ledger containing exactly one balanced transaction. Ledger algebra users in Recognition Science cite it for base cases when inducting over transaction sequences or verifying conservation in single-event models. The definition is a direct record constructor that copies the transaction's debit, credit, and balance fields into the ledger structure.
Claim. For a transaction $t$ with debit $d$, credit $c$, and $d + c = 0$, the singleton ledger is the structure whose transaction list is $[t]$, total debit equals $d$, total credit equals $c$, and global balance is the proof $d + c = 0$.
background
The Ledger structure is a list of transactions together with derived totals and a global balance constraint that enforces conservation. A Transaction is a pair of integer debit and credit amounts required to sum to zero. The RRF Foundation module presents the ledger as the algebraic carrier for double-entry bookkeeping, where every conservation law (energy, charge, momentum) appears as an instance of ledger closure.
proof idea
One-line record construction that sets transactions to the list containing the input transaction, total_debit to its debit field, total_credit to its credit field, and global_balance to its balanced field.
why it matters
Singleton supplies the base case for ledger construction and is invoked by downstream results including clauseUnit_correct, reality_forced_by_any_distinction, and floor_status. It realizes the conservation laws that the module doc-comment identifies as instances of ledger closure, supporting the forcing-chain steps that derive physical structure from accounting constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.