addEvent
plain-language theorem explainer
Posts one recognition event onto a rational ledger together with its reciprocal, enforcing double-entry. Cosmogenesis and the flow-product conservation proofs cite it as the atomic ledger update. The definition is the two-cons list prepend of the event and its source/target-swapped inverse-ratio partner.
Claim. Given a list $L$ of rational recognition events and an event $e=(s,t,r)$, return the list with $e$ and its reciprocal $(t,s,r^{-1})$ prepended: $\mathrm{add}(L,e)=e::(t,s,r^{-1})::L$.
background
This module is the computable, kernel-checked mirror of the real cosmogenesis in PreBigBang and FirstTick. Events live over $\mathbb{Q}$ so the simulation is #eval-able and conservation is proved in the kernel.
A QEvent is a triple (source agent, target agent, positive rational ratio), the rational mirror of LedgerForcing.RecognitionEvent. The reciprocal map swaps source and target and inverts the ratio, matching the ledger reciprocal automorphism from CostAlgebra and LedgerForcing.
Double-entry is the Recognition ledger rule: every posted distinction is accompanied by its inverse so the multiplicative flow product at each agent is unchanged ($r\cdot r^{-1}=1$). The eight-tick octave (T7) builds the full cosmogenesis ledger by iterating this update.
proof idea
Pure definition: prepend the event and then its reciprocal onto the existing list. No tactics or lemmas; the body is the two-cons expression e :: qreciprocal e :: es. Downstream theorems unfold this definition and simplify.
why it matters
Atomic ledger step for the rational cosmogenesis simulation. Downstream, qcost_addEvent shows each paired post raises total J-cost by exactly $2J(r)$, mirroring FirstTick.ledger_cost_add_event. flowProduct_addEvent is the conservation step: the flow product is invariant under the update. Folding eight such posts yields cosmogenesis, and flowProduct_foldl / cosmogenesis_conserves prove the flow product is identically 1 at every agent after the full 8-tick run (T7 octave).
Also feeds length lemmas (addEvent_length, foldl_addEvent_length): $n$ paired posts give $2n$ events. Without this double-entry constructor the rational conservation and cost-increment chain cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.