addEvent_length
plain-language theorem explainer
Each double-entry posting of a rational recognition event appends both the event and its reciprocal, so ledger length grows by exactly two. Cosmogenesis simulation proofs cite this when counting events after n ticks. The argument is a one-line simplification of the paired-posting definition.
Claim. For any finite list $L$ of rational recognition events and any event $e$, the length of the list obtained by posting $e$ together with its reciprocal equals $|L|+2$.
background
The module supplies a computable, kernel-checked mirror of cosmogenesis over $\mathbb{Q}$, parallel to the real-valued dynamics in PreBigBang and FirstTick. Recognition events are structures with natural-number source and target and a rational ratio; the reciprocal swaps endpoints and inverts the ratio.
Paired posting implements double-entry bookkeeping: one call prepends both the event and its reciprocal. The same module tracks summed $J$-cost and the multiplicative flow product at each agent; double-entry multiplies the flow by $r\cdot r^{-1}=1$, so conservation is exact over rationals.
Upstream, the posting operation is the direct mirror of the real ledger's add-event. List length here is ordinary finite-list cardinality, not the trace-length of the primitive recognition calculus.
proof idea
One-line wrapper: simp unfolds the definition of paired posting, which is literally $e$ consed onto the reciprocal of $e$ consed onto $L$. List-length arithmetic then yields $|L|+2$ with no further lemmas.
why it matters
Feeds the fold lemma that a ledger built by $n$ paired postings from the empty list has exactly $2n$ events. That count is the bookkeeping backbone of the eight-tick cosmogenesis simulation: cost increments by $2J(r)$ per tick, and the flow product stays identically $1$ at every agent for any positive rational seed.
In the broader Recognition chain this sits under the computable mirror of FirstTick ledger dynamics, not under T0–T8 forcing itself. It makes the double-entry invariant and the Fibonacci convergents toward $\varphi$ inspectable by #eval with a kernel proof rather than a runtime check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.