qcost_addEvent
plain-language theorem explainer
Posting one double-entry recognition event (the event plus its reciprocal) raises total ledger J-cost by exactly twice J of the event ratio. Cosmogenesis and ledger-cost arguments over rationals cite this as the per-tick cost increment. The proof unfolds the cost and posting definitions, applies reciprocal symmetry of J, and finishes by ring.
Claim. For any finite list $L$ of rational recognition events and any event $e$ with ratio $r\in\mathbb{Q}$, if one posts $e$ together with its reciprocal (source/target swapped, ratio inverted), the total ledger cost satisfies $\mathrm{cost}(L\cup\{e,e^{\mathrm{rec}}\})=\mathrm{cost}(L)+2\,J(r)$, where $J(x)=(x+x^{-1})/2-1$.
background
This module is a computable, kernel-checked mirror of cosmogenesis over $\mathbb{Q}$. Real-valued dynamics live in PreBigBang and FirstTick; here the same ledger is realized so that simulation is a Lean object one can evaluate, with conservation proved in the kernel.
A recognition event carries source, target, and a rational ratio. The cost functional is the canonical $J(x)=(x+x^{-1})/2-1$ (the T5 unique cost). Total ledger cost is the sum of $J$ over event ratios. Posting is double-entry: one event is always accompanied by its reciprocal (swap endpoints, invert the ratio). Reciprocal symmetry $J(x^{-1})=J(x)$ is already proved in-module, so each paired post contributes two equal $J$ terms.
The module doc states that this increment mirrors FirstTick.ledger_cost_add_event and that the conserved multiplicative invariant (flow product) is handled separately: double-entry multiplies by $r\cdot r^{-1}=1$.
proof idea
Term-style tactic proof. Unfold total cost and the double-entry posting constructor (event consed with its reciprocal onto the list). Simplify the mapped sum under List.map_cons and List.sum_cons, substituting the reciprocal definition and the already-proved identity $J(x^{-1})=J(x)$. The resulting rational expression is $J(r)+J(r^{-1})+\mathrm{cost}(L)$; ring rewrites it to $\mathrm{cost}(L)+2J(r)$.
why it matters
Gives the exact per-tick cost step in the rational cosmogenesis simulation: each paired distinction adds $2J(r)$ to the ledger. That is the computable counterpart of the real ledger-cost increment used in FirstTick, so cost accounting over the eight-tick octave stays kernel-checked rather than runtime-only.
It sits next to the flow-product conservation story in the same module: cost grows by a controlled $J$-increment while the multiplicative $\sigma$-invariant stays fixed under double-entry. Downstream usage is not yet wired in this graph snapshot, but the module framing ties it to full 8-tick cosmogenesis and to the rational Fibonacci recurrence that exhibits $\varphi$ as exact convergents. Framework landmarks: T5 $J$-uniqueness and the eight-tick (T7) ledger structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.