flowContribution
plain-language theorem explainer
An event contributes its rational ratio to an agent's flow if that agent is the event's source or target, and contributes the unit factor 1 otherwise. Cosmogenesis and ledger-conservation arguments cite this as the per-event factor in the multiplicative conserved quantity σ. The body is a one-line incidence conditional over ℚ.
Claim. For an agent $a \in \mathbb{N}$ and a recognition event $e$ over $\mathbb{Q}$ with fields $(\mathrm{source},\mathrm{target},r)$, the flow contribution of $e$ at $a$ is $r$ if $a$ equals the source or the target of $e$, and equals $1$ otherwise.
background
This module supplies a computable, kernel-checked mirror of cosmogenesis over $\mathbb{Q}$. The real-valued dynamics live in PreBigBang and FirstTick; here the same ledger is realized so that conservation is a proved identity rather than a runtime check, and sequences can be #eval'd.
A recognition event over $\mathbb{Q}$ is a triple (source, target, ratio). Reciprocal posting swaps endpoints and inverts the ratio (double-entry). The conserved quantity $\sigma$ is taken in multiplicative form: at each agent, multiply the ratios of all events that touch that agent. Double-entry multiplies by $r \cdot r^{-1} = 1$, so the product is invariant and targets the conserved value $1$.
This definition is the per-event factor in that product: incidence selects the ratio, non-incidence contributes the multiplicative identity.
proof idea
Pure definition, not a theorem. The body is a single conditional: if the agent equals the event source or target, return the event's rational ratio; else return $1$. No lemmas are applied. Downstream proofs (pair cancellation, list products) unfold this definition and case-split on the same incidence predicate.
why it matters
This is the atomic factor of the multiplicative conserved flow. It feeds the flow product (product over a list of events of these contributions), which is the computable form of $\sigma$ with conserved value $1$. It also feeds the pair lemma: an event and its reciprocal contribute a factor of exactly $1$ at every agent, either both touch (factor $r \cdot r^{-1}$) or neither does (factor $1$).
That pair identity is what makes double-entry posting preserve the flow product, and what lets the module prove that after the full eight-tick cosmogenesis the flow product is exactly $1$ at every agent for any positive seed. In the Recognition chain this sits with the eight-tick octave (T7) and the rational self-similar recurrence whose Fibonacci convergents approach $\varphi$ (T6), all visible over $\mathbb{Q}$ without decide or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.