paired_preserves_balance
plain-language theorem explainer
Appending a ledger event and its conjugate to a balanced ledger page produces another balanced page. Algebraists building invariant structures for Recognition Science ledgers cite this when extending zero-balance pages. The proof reduces the balance predicate via case analysis on the page, simplification of the fold-based sum, and integer arithmetic.
Claim. Let $P$ be a ledger page whose event list $E$ satisfies $computeBalance(E)=0$. For any ledger event $e$, the page formed by the event list $E ++ [e, -e]$ with balance field reset to 0 is balanced.
background
A ledger page is a finite list of ledger events paired with an integer balance field that defaults to the sum of flows. Each ledger event is a signed integer flow, with positive values denoting debit and negative values credit; the group operation is ordinary addition on these integers. The conjugate of an event $e$ is defined as its negation $-e$, supplying the natural pairing that cancels net flow.
proof idea
The proof begins with case analysis on the ledger page to expose its events and balance components. It then applies simplification to unfold IsBalanced, computeBalance, list append, and the conjugate definition. The resulting integer equation is discharged directly by the omega tactic.
why it matters
The result supplies a basic closure property for balanced ledger pages under paired extensions, supporting the algebraic layer that encodes conservation in Recognition Science models. It precedes the eight-window constraint section in the same module and aligns with the broader ledger factorization used in upstream DAlembert and nucleosynthesis tiers. No immediate downstream theorems are recorded, leaving its role as a reusable building block for graded or windowed ledger constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.