flowProduct
plain-language theorem explainer
The flow product at a given agent is the product of every event's contribution to that agent. It is the multiplicative, rational form of the conserved ledger quantity σ, whose invariant value is 1. Cosmologists and ledger theorists cite it when proving σ-conservation through the eight-tick cosmogenesis. The definition is a one-line map-then-product over the event list.
Claim. For a finite list of recognition events $E$ over $\mathbb{Q}$ and an agent $a\in\mathbb{N}$, the flow product is $\prod_{e\in E} c_a(e)$, where the contribution $c_a(e)$ equals the event ratio $r_e$ if $e$ touches $a$ (as source or target) and equals $1$ otherwise.
background
This module supplies a computable mirror of cosmogenesis over $\mathbb{Q}$, parallel to the real-valued dynamics in PreBigBang and FirstTick. Recognition events are rational triples (source, target, ratio). Double-entry posting always inserts an event together with its reciprocal (swapped endpoints, inverted ratio), so the ledger stays balanced.
An event's contribution at agent $a$ is the ratio when the event touches $a$, and $1$ otherwise. The flow product multiplies those contributions across the whole event list. It is the multiplicative form of the conserved quantity $\sigma$: under paired posting one multiplies by $r\cdot r^{-1}=1$, so the product is invariant. The empty ledger has product $1$ at every agent.
Upstream, this mirrors the real ledger's add-event and reciprocal constructions in LedgerForcing, restricted to rationals so the simulation is kernel-checkable and #eval-able.
proof idea
Pure definition: map each event through the agent-local contribution function, then take the list product in $\mathbb{Q}$. No proof obligations. Downstream lemmas unfold this definition and cancel paired factors via the contribution-pair identity.
why it matters
This is the conserved observable of the rational cosmogenesis simulation. The conservation step shows that posting a paired event leaves the product unchanged at every agent. Folding that step from the empty ledger yields product exactly $1$ after any number of paired posts with nonzero ratios. The main theorem then specializes to the full eight-tick cosmogenesis: for any positive seed and any agent, the flow product equals $1$, with no decide and no sorry.
Trace certificates for the canonical seed-2 run record the product at agent $0$ as one of the kernel-checked fields. The eight-tick cadence matches the T7 octave landmark. The same run produces Fibonacci convergents of the self-similar recurrence, making the emergence of $\varphi$ visible as an exact rational sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.