IsBalanced
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not constrain the internal structure of LedgerEvent.
- Does not extend to infinite event lists.
- Does not incorporate external forcing conditions from the unified chain.
- Does not compute numerical values for specific constants.
Lean usage
theorem empty_is_balanced : IsBalanced ⟨[], 0⟩ := by simp [IsBalanced, computeBalance]formal statement (Lean)
93def IsBalanced (page : LedgerPage) : Prop :=
proof body
Definition body.
94 computeBalance page.events = 0
95
96/-- The empty page is balanced. -/