balanced
plain-language theorem explainer
The definition states that a ledger L is balanced exactly when its sequence of recognition events meets the count-reciprocal condition for every event. Algebraists and complexity theorists modeling computation via ledgers cite this when proving conservation or separation results. It is realized as a one-line abbreviation delegating directly to the balanced_list predicate.
Claim. A ledger $L$ with event list $E$ is balanced if and only if for every recognition event $e$, the multiplicity of $e$ in $E$ equals the multiplicity of its reciprocal in $E$.
background
The Ledger Forcing module establishes that J-symmetry forces double-entry ledger structure. A Ledger is the structure whose fields are a list of RecognitionEvent together with the double_entry constraint requiring that list to be balanced. The upstream balanced_list predicate asserts that a list $l$ satisfies the condition that for every event $e$, the count of $e$ equals the count of reciprocal($e$).
proof idea
The definition is a one-line wrapper that applies the balanced_list predicate to the events field of the supplied Ledger.
why it matters
This supplies the predicate used by LedgerAlgebra to define IsBalanced and computeBalance, and appears in downstream arguments that ledger structure forces separation in computation models such as ledger_forces_separation. It realizes the double-entry constraint required by the module claim that J-symmetry implies double-entry bookkeeping, closing the step from J-uniqueness to the eight-tick octave by enforcing reciprocity at the ledger level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.