add_event
plain-language theorem explainer
Adding a recognition event and its reciprocal to an existing ledger yields a new ledger whose event list is extended by the pair while the double-entry constraint is inherited from the balance preservation theorem. Model builders constructing finite Euler ledgers from prime lists or computing ledger costs cite this operation. The definition is a direct record update that applies the list-balance theorem to witness the new double_entry field.
Claim. Let $L$ be a ledger and $e$ a recognition event with positive ratio. The updated ledger has event list $e :: e^{-1} :: L.events$ and satisfies the balance predicate by the theorem that adjoining any event together with its reciprocal preserves balance on lists.
background
A ledger is a list of recognition events equipped with a witness that the list is balanced under the double-entry rule. A recognition event is a triple of source agent, target agent, and positive real ratio; the reciprocal swaps source and target while inverting the ratio. The module Ledger Forcing derives double-entry structure from J-symmetry of the recognition cost function J(x) = (x + x^{-1})/2 - 1.
proof idea
The definition is a one-line record constructor. It populates the events field by consing the given event, its reciprocal, and the prior list. The double_entry field is supplied directly by the theorem add_event_balanced_list applied to the prior list and its balance witness.
why it matters
This definition supplies the inductive step used by finiteEulerLedger and add_event_cost_formula in ConcreteEulerLedger, where each prime contributes a paired event whose cost contribution is exactly twice the single-event cost. It realizes the ledger-forcing principle that J-symmetry forces double-entry accounting, feeding the parent theorem add_event_balanced that asserts the result remains balanced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.