flowProduct_nil
plain-language theorem explainer
The empty event list has flow product equal to 1 at every agent. Cosmogenesis and ledger-conservation arguments cite this as the multiplicative base case of the rational σ invariant. The proof is a one-line simplification of the product definition on the empty list.
Claim. For every agent $a \in \mathbb{N}$, the flow product of the empty list of rational recognition events evaluated at $a$ equals $1$.
background
This module supplies a computable $\mathbb{Q}$-mirror of the PreBigBang/FirstTick cosmogenesis dynamics. Recognition events are rational (QEvent); double-entry posting inserts each event with its reciprocal (source/target swapped, ratio inverted). The conserved quantity $\sigma$ is written multiplicatively as the flow product at an agent: the product, over the event list, of that agent's flow contribution from each event. Its conserved value is $1$.
By definition the flow product is (es.map (flowContribution agent)).prod. On the empty ledger there are no contributions, so the product is the empty product in $\mathbb{Q}$. This nil identity is the starting point before any addEvent steps; double-entry later multiplies by $r \cdot r^{-1} = 1$, preserving the value.
proof idea
One-line wrapper: simp [flowProduct] unfolds the definition to the product of the mapped contributions. The empty list maps to the empty list, and the empty product in $\mathbb{Q}$ is definitionally $1$. No further lemmas are required.
why it matters
Base case for the multiplicative conservation law in the rational cosmogenesis simulation. The module's main conservation theorem (cosmogenesis_conserves) asserts that after the full eight-tick run the flow product remains exactly $1$ at every agent for any positive seed, with a kernel proof (no decide, no sorry). Sibling lemmas (flowProduct_addEvent, flowContribution_pair, qcost_addEvent) handle the inductive step under double-entry posting.
This sits inside the eight-tick octave structure (forcing chain T7) and the computable emergence of $\varphi$: the self-similar recurrence $r \mapsto 1 + 1/r$ over $\mathbb{Q}$ produces the Fibonacci convergents visible under #eval. The empty-ledger identity anchors that the invariant starts at the conserved value before any ticks fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.