paired_event_sum_zero
plain-language theorem explainer
Paired events in the ledger algebra cancel exactly under addition, confirming the double-entry principle for signed integer flows. Researchers assembling the algebraic core of the Recognition Science ledger cite this when verifying conservation at vertices. The proof performs case analysis on the LedgerEvent constructor and reduces the sum via integer arithmetic.
Claim. For every ledger event $e$, $e + e.conj = 0$, where $e.conj$ is the conjugate event obtained by negating the integer flow of $e$.
background
A ledger event is a signed integer flow on an edge, with positive values as debits and negative values as credits. The structure equips these flows with componentwise addition, negation, and zero, making the events into an abelian group isomorphic to $(ℤ, +, 0)$. Conjugation is implemented as negation, so the conjugate of an event with flow $f$ is the event with flow $-f$.
proof idea
The proof is a term-mode case split on the LedgerEvent constructor that extracts the underlying flow integer. It rewrites the sum as the event whose flow is $f + (-f)$, which equals the zero event, then applies simp to conclude the equality.
why it matters
This supplies the paired-cancellation clause inside the ledger_algebra_certificate theorem, which records the six core ledger properties including abelian group structure, involutive conjugation, and vertex conservation. The identity directly enables the double-entry bookkeeping that forces net flux to vanish, feeding the graded ledger construction used later in the simplicial ledger and mechanism-design layers of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.