IsBalanced
plain-language theorem explainer
Ledger pages are balanced exactly when the net flow across their events sums to zero. Algebraists working on ledger models cite this definition when establishing closure under empty initialization and event pairing. The definition reduces the balance predicate to an integer equality via the computeBalance fold. It serves as the base case for inductive arguments on ledger pages.
Claim. Let $p$ be a ledger page with event list $E$. Then $p$ is balanced if the sum of flows over $E$ equals zero.
background
The LedgerPage structure packages a list of LedgerEvent items, each with an integer flow value, and maintains a balance field computed as the fold-left sum of those flows. computeBalance performs the identical summation on the events list. This definition in LedgerAlgebra mirrors the balanced predicate from LedgerForcing, which applies the same zero-sum condition to general ledgers. The local setting treats pages as atomic units for algebraic manipulations of balance.
proof idea
The declaration is a direct definition that sets the balanced property equal to the condition that computeBalance applied to the page events yields zero. No tactics or lemmas are invoked beyond the abbreviation itself.
why it matters
This definition is the target of empty_balanced and paired_preserves_balance, which show preservation under initialization and conjugation. It also supports balanced_iff_zero_debt in the Ramanujan bridge. Within Recognition Science it provides the algebraic foundation for ledger neutrality, linking to the forcing chain steps that enforce self-similar fixed points and three-dimensional space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.