LedgerEvent
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assign physical units or dimensions to flow values.
- Does not incorporate J-cost, defect distance or the phi-ladder.
- Does not treat infinite or continuous ledgers.
- Does not prove balance preservation without further structure.
formal statement (Lean)
55structure LedgerEvent where
56 /-- The flow value (positive = debit, negative = credit) -/
57 flow : ℤ
58deriving DecidableEq, Repr
59
60instance : Add LedgerEvent := ⟨fun e₁ e₂ => ⟨e₁.flow + e₂.flow⟩⟩
proof body
Definition body.
61instance : Neg LedgerEvent := ⟨fun e => ⟨-e.flow⟩⟩
62instance : Zero LedgerEvent := ⟨⟨0⟩⟩
63
64/-- The conjugate (paired) event: ē = −e. -/
65def LedgerEvent.conj (e : LedgerEvent) : LedgerEvent := ⟨-e.flow⟩
66
67/-- **PROVED: Paired events sum to zero (double-entry).** -/