computeBalance
plain-language theorem explainer
The definition aggregates integer flows from a sequence of ledger events to yield their net sum. Ledger algebraists in Recognition Science cite it to support balance verification in forcing constructions. Realization occurs through a left fold that adds each event's flow value to an accumulator initialized at zero.
Claim. For a list of ledger events where each carries a signed integer flow, the balance equals the sum of all flows.
background
The LedgerEvent structure models a signed integer flow on an edge, positive for debit and negative for credit, equipped with the additive group structure on the integers. This definition computes the total flow sum for any list of such events. It draws on the balanced definition from LedgerForcing, which checks if a ledger's events sum to zero, and various A abbreviations denoting one active edge per fundamental tick across modules.
proof idea
The definition is given directly by a left fold that starts with zero and successively adds the flow component of each ledger event in the list. No lemmas are applied beyond the standard list fold operation and the structure accessor.
why it matters
It serves as the computational core for the IsBalanced definition and enables the empty_balanced theorem along with paired_preserves_balance, which establish invariance of zero balance under empty lists and conjugate event pairs. This supports ledger constructions in the forcing chain leading to D=3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.