flowContribution_pair
plain-language theorem explainer
An event and its reciprocal multiply to unit flow contribution at every agent: either both touch the agent and give r·r⁻¹=1, or neither does and the product is 1·1=1. Cosmogenesis and ledger-conservation arguments cite this as the local cancellation step. The proof is a two-branch case split on whether the agent is incident, then mul_inv_cancel₀ or ring.
Claim. For any rational recognition event $e$ with nonzero ratio $r$ and any agent $a$, the product of the flow contributions of $e$ and of its reciprocal (source/target swapped, ratio $r^{-1}$) equals $1$.
background
This module is the computable $\mathbb{Q}$-mirror of cosmogenesis: events, double-entry posting, and the conserved multiplicative flow live over rationals so the simulation is kernel-checkable and #eval-able. A QEvent is a triple (source, target, ratio) over $\mathbb{Q}$, mirroring the real ledger recognition event. Its reciprocal swaps endpoints and inverts the ratio.
Flow contribution at an agent is the event's ratio when the agent is source or target, and $1$ otherwise. The flow product is the product of those contributions over a list of events; it is the multiplicative, computable form of the conserved $\sigma$, with conserved value $1$. Double-entry posting always appends an event together with its reciprocal, so local $r\cdot r^{-1}=1$ cancellation is the mechanism of invariance.
Upstream, the contribution and reciprocal defs fix the case structure used here; the real-side FirstTick ledger cost increment is the additive twin of this multiplicative story.
proof idea
Unfold contribution and reciprocal. Case on whether the agent is incident to $e$ (source or target).
If yes, the reciprocal is also incident (endpoints swapped), so both branches return the ratio and its inverse; mul_inv_cancel₀ with the nonzero-ratio hypothesis gives $1$.
If no, neither endpoint matches, so both contributions are $1$; ring closes $1\cdot 1=1$. The second if_neg uses that incidence fails for the reciprocal exactly when it fails for $e$ (symmetry of $\lor$).
why it matters
This is the atomic cancellation behind ledger conservation in the rational cosmogenesis sim. Downstream, flowProduct_addEvent multiplies the two new contributions into the product and rewrites by this lemma plus one_mul, proving that posting a paired event leaves every agent's flow product unchanged.
That conservation step feeds the module's main claim: after the full eight-tick cosmogenesis the flow product is exactly $1$ at every agent for any positive seed, with no decide and no sorry. The eight-tick octave (forcing T7) is thus visible as an exact rational invariant, not only a runtime check.
In the broader RS ledger picture, double-entry ($e$ with reciprocal) is the discrete recognition of balanced exchange; the multiplicative unit factor is the computable twin of cost additivity $+2J(r)$ on the real side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.