flowProduct_addEvent
plain-language theorem explainer
Posting a recognition event together with its reciprocal leaves every agent's flow product unchanged. Cosmology and ledger authors cite this as the single-step conservation law for the multiplicative σ (flow product) in the rational cosmogenesis simulation. The proof unfolds the product, applies the pair-contribution identity r·r⁻¹=1, and cancels the leading 1.
Claim. Let $L$ be a list of rational recognition events and let $e$ be an event with ratio $r\neq 0$. For every agent $a\in\mathbb{N}$, the flow product at $a$ after double-entry posting of $e$ (event plus reciprocal) equals the flow product at $a$ on $L$: $\mathrm{flowProduct}(\mathrm{addEvent}(L,e),a)=\mathrm{flowProduct}(L,a)$.
background
This module is the computable, kernel-checked mirror of PreBigBang/FirstTick cosmogenesis, run over $\mathbb{Q}$ so the ledger can be #eval'd. A QEvent is a recognition event (source, target, rational ratio). Double-entry posting addEvent prepends both $e$ and its reciprocal (swap endpoints, invert ratio).
The conserved quantity $\sigma$ is written multiplicatively as the flow product at an agent: the product, over all events, of each event's contribution (the ratio if the agent is an endpoint, else $1$). Conserved value is $1$. Upstream, flowContribution_pair already shows that an event and its reciprocal contribute a factor of exactly $1$ at every agent: either both touch it ($r\cdot r^{-1}=1$) or neither does (factor $1$).
proof idea
Unfold flowProduct and addEvent, so the new product is the product of contributions of $e$, of its reciprocal, and of the old list. List.map_cons / List.prod_cons expose the two leading factors. Reassociate with mul_assoc, replace the pair by $1$ via flowContribution_pair e he agent, then cancel with one_mul. The nonzero-ratio hypothesis is exactly what the pair lemma needs for $r\cdot r^{-1}=1$.
why it matters
This is the inductive step for multiplicative conservation under double-entry. Downstream, flowProduct_foldl uses it to prove that any ledger built solely by addEvent from the empty list has flow product $1$ at every agent (nonzero ratios). That fold identity is the engine behind cosmogenesis_conserves: after the full eight-tick cosmogenesis the flow product remains exactly $1$ for any positive seed, with no decide and no sorry.
In the Recognition framework this is the rational, computable form of ledger $\sigma$-conservation that mirrors FirstTick's real dynamics. It sits under the eight-tick octave (T7) story: the same double-entry that forces $+2J(r)$ cost per tick multiplies the flow by $r\cdot r^{-1}=1$, so cost accrues while the multiplicative invariant stays fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.