flow_contribution
plain-language theorem explainer
flow_contribution returns the signed log-ratio contribution of one recognition event to a given agent, or zero when the agent is uninvolved. Ledger conservation arguments cite it as the atomic term whose sum vanishes under balance. The definition is a direct conditional on source or target membership.
Claim. Let $e$ be a recognition event with positive ratio $r$ between agents $s$ and $t$. For any agent $a$, the flow contribution of $e$ to $a$ equals $log r$ if $a=s$ or $a=t$, and equals $0$ otherwise.
background
The LedgerForcing module shows that J-symmetry forces double-entry ledger structure. RecognitionEvent records a directed recognition with source, target, and positive real ratio. The reciprocal operation swaps source and target while replacing the ratio by its inverse. Upstream results supply the reciprocal automorphism from CostAlgebra and the RecognitionEvent structure itself.
proof idea
Direct definition via conditional: the value is Real.log of the ratio exactly when the agent equals source or target, otherwise zero. No lemmas or tactics are invoked.
why it matters
The definition supplies the summand used by conservation_from_balance to prove that balanced ledgers have zero net flow for every agent. It thereby realizes the double-entry consequence of J-symmetry inside the Recognition framework, where the eight-tick octave and RCL already fix the underlying algebraic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.