computeBalance
The computeBalance definition sums the integer flow values across a list of ledger events to produce the net balance. Algebraists verifying ledger neutrality within Recognition Science would cite it when establishing the zero-sum condition for balanced pages. It is realized as a direct left-fold that accumulates each event's flow component starting from zero.
claimLet $E = (e_1, e_2, ..., e_n)$ be a finite list of ledger events, where each $e_i$ is a structure carrying an integer flow $f_i$. Then computeBalance$(E) := f_1 + f_2 + ... + f_n$.
background
LedgerEvent is a structure with a single field flow : ℤ, equipped with addition, negation and zero so that the events form the additive group (ℤ, +, 0). Positive flow records a debit and negative flow a credit on an edge. The definition lives in the LedgerAlgebra module that supplies the elementary operations for ledger pages used in the forcing construction. It is invoked by the balanced predicate of LedgerForcing and by the IsBalanced definition that tests whether the summed value equals zero. Upstream results include the LedgerEvent group structure and the active-edge count A appearing in related mass and modal modules.
proof idea
The definition is a one-line wrapper that applies List.foldl to the addition operation on the flow components, starting from the integer zero.
why it matters in Recognition Science
computeBalance supplies the concrete summation that IsBalanced, empty_balanced and paired_preserves_balance depend on to certify neutrality of ledger pages. It thereby supports the ledger-forcing claim that every ledger is balanced by construction. In the Recognition framework it operationalizes the zero-balance condition required for the eight-tick octave and the D = 3 spatial-dimension step.
scope and limits
- Does not prove any invariance or preservation properties of the balance.
- Does not relate the computed sum to J-cost, defect distance or the phi-ladder.
- Does not extend to infinite lists or non-integer flows.
Lean usage
theorem empty_is_zero : computeBalance [] = 0 := rflformal statement (Lean)
89def computeBalance (events : List LedgerEvent) : ℤ :=
proof body
Definition body.
90 events.foldl (fun acc e => acc + e.flow) 0
91
92/-- A **balanced ledger page** has σ = 0. -/