IsBalanced
A ledger page is balanced when the total sum of flows across its events equals zero. Modelers of algebraic ledgers in Recognition Science cite this definition when establishing neutrality conditions for forcing constructions and windowed balance checks. The declaration is a direct definition that equates the fold-based balance computation to zero, serving as the base predicate for preservation and emptiness results.
claimA ledger page $p$ is balanced if the total flow sum satisfies $s(p) = 0$, where $s(p)$ is the integer sum of flow values over the finite list of events in $p$.
background
The LedgerAlgebra module defines a LedgerPage as a structure containing a finite list of LedgerEvents together with an integer balance field computed by folding the flow values. The companion computeBalance function extracts precisely this sum from the event list. This local definition sits inside the algebra layer that supports ledger forcing, inheriting the zero-sum notion of balance from the upstream LedgerForcing module.
proof idea
The declaration is a direct definition that sets IsBalanced page to the proposition computeBalance page.events = 0. No lemmas or tactics are applied; the body simply reuses the foldl sum already present in computeBalance.
why it matters in Recognition Science
This predicate anchors the algebra of balanced ledgers and is invoked by the downstream theorems empty_balanced and paired_preserves_balance inside the same module, as well as by balanced_iff_zero_debt in the RamanujanBridge. It supplies the neutrality condition required for zero-debt windows and eight-tick constructions in the broader Recognition framework.
scope and limits
- Does not specify the internal structure or types of individual LedgerEvents.
- Does not address infinite lists or continuous-time ledgers.
- Does not compute or bound numerical flow values for concrete events.
- Does not connect directly to J-cost, phi-ladder, or spatial dimension forcing.
Lean usage
theorem empty_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. -/