flow_contribution
plain-language theorem explainer
The definition returns the logarithmic contribution of one recognition event to an agent's net flow. Ledger conservation proofs cite it to decompose total flow into per-event terms before applying reciprocity. Implementation is a direct conditional that applies Real.log to the event ratio exactly when the agent is source or target.
Claim. Let $e$ be a recognition event with positive ratio $r$. For agent $a$, the contribution equals $log r$ if $a$ is the source or target of $e$, and equals zero otherwise.
background
RecognitionEvent is the structure carrying source agent, target agent, and positive real ratio that models a directed recognition step. The LedgerForcing module shows that J-symmetry on such events forces a double-entry ledger structure. The reciprocal operation defined in the same module swaps source and target while inverting the ratio, supplying the negation property used downstream.
proof idea
Direct definition. The body is an if-then-else that tests membership of the agent in the event's source or target pair and returns Real.log of the ratio or zero.
why it matters
Supplies the summand for net_flow inside conservation_from_balance, which proves that balanced ledgers (every event paired with its reciprocal) have zero net flow for every agent. This step closes the argument that J-symmetry implies double-entry bookkeeping. The same term appears in the companion reciprocity lemma that shows flow_contribution(e) + flow_contribution(reciprocal e) = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.