LedgerEvent
plain-language theorem explainer
A ledger event is defined as a signed integer flow on an edge, positive for debit and negative for credit, equipped with the abelian group operations of addition, negation and zero. Algebraic modelers of conservation in Recognition Science cite it as the atomic object for double-entry ledgers. The construction is a direct structure declaration that lifts the integer group operations and adds a conjugation map given by negation.
Claim. A ledger event is an element $f$ of the additive group of integers, written with positive values for debits and negative values for credits, together with the induced operations of addition, negation and zero.
background
The LedgerAlgebra module builds an algebraic model of double-entry bookkeeping inside the Recognition framework. A ledger event is introduced as a signed integer flow; the module then equips it with the group structure of the integers and defines conjugation as negation. The local setting is the construction of finite ledgers, pages and neutral windows that enforce net flux zero at every vertex.
proof idea
The declaration is a structure with a single integer field. Additive, negation and zero instances are obtained by direct delegation to the corresponding operations on the flow value. Conjugation is introduced as the map sending each event to the negation of its flow.
why it matters
LedgerEvent supplies the basic type used by computeBalance, conj_involution, neutralWindow and the ledger_algebra_certificate. The certificate records that events form an abelian group, conjugation is an involution, and paired events sum to zero, thereby grounding the conservation statements that appear later in graded ledgers and eight-window neutrality. It therefore occupies the algebraic foundation step that precedes the eight-tick octave and vertex conservation arguments in the Recognition chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.