ledger_balanced
Every ledger built from recognition events carries a double-entry constraint by the definition of its structure, so its net flow vanishes identically. Researchers deriving double-entry bookkeeping from J-symmetry in Recognition Science cite this when closing the ledger-forcing step. The proof is a one-line projection that extracts the balanced_list field already present in the Ledger record.
claimLet $L$ be any ledger whose events are a list of recognition events equipped with a double-entry constraint. Then the net balance of $L$ is zero: balanced$(L)$ holds.
background
The module LedgerForcing shows that J-symmetry forces double-entry ledger structure. A Ledger is a structure containing a list of RecognitionEvent together with a field double_entry : balanced_list events. The auxiliary definition balanced states that a ledger is balanced precisely when balanced_list holds of its event list. Upstream results supply the net-balance functions (net in RRF.Core.Strain and RRF.Foundation.Ledger) that are required to be zero for closed ledgers.
proof idea
The proof is a one-line wrapper that applies the double_entry projection: ledger_balanced L := L.double_entry. No further lemmas or tactics are invoked; the balanced predicate is discharged directly by the constructor field of the Ledger record.
why it matters in Recognition Science
This theorem supplies the base case that every Ledger is balanced by construction, which is invoked by finiteEulerLedger_balanced to conclude that every finite Euler ledger has zero net flow. It therefore closes the ledger-forcing step inside the J-symmetry to double-entry chain (T5–T8 landmarks) and confirms that the Recognition Composition Law produces ledgers whose total debit equals total credit.
scope and limits
- Does not construct or guarantee the existence of any particular ledger.
- Does not address infinite or non-list event collections.
- Does not derive the balanced_list predicate from J-symmetry; that step occurs upstream.
- Does not compute numerical values of net flow; only asserts the zero predicate.
Lean usage
theorem finiteEulerLedger_balanced ... := LedgerForcing.ledger_balanced _formal statement (Lean)
96theorem ledger_balanced (L : Ledger) : balanced L := L.double_entry
proof body
Term-mode proof.
97
98/-- The net flow at an agent. -/