flow_contribution
This definition computes the signed logarithmic contribution of one recognition event to an agent's net flow, returning log(ratio) precisely when the agent is source or target. Ledger-balance proofs in the Recognition Science framework cite it to decompose aggregate flows into per-event terms before invoking reciprocity. The implementation is a direct conditional expression on agent membership.
claimFor a recognition event $e$ with source $s$, target $t$ and positive ratio $r$, the flow contribution to agent $a$ equals $log r$ if $a=s$ or $a=t$, and equals $0$ otherwise.
background
The LedgerForcing module shows that J-symmetry on recognition events forces double-entry ledger structure. RecognitionEvent is the structure carrying source agent, target agent and positive real ratio. The reciprocal operation on events swaps source and target while inverting the ratio, as defined in the same module and in CostAlgebra.reciprocal.
proof idea
Direct definition via if-then-else that tests membership of the agent in the event's source or target field and returns the real logarithm of the ratio or zero.
why it matters in Recognition Science
The definition supplies the per-event term used by conservation_from_balance (net flow vanishes on balanced ledgers) and by flow_contribution_reciprocal (contribution negates under reciprocity). It thereby supports the double-entry property that follows from J-symmetry and the Recognition Composition Law in the T0-T8 forcing chain.
scope and limits
- Does not aggregate contributions across a list of events.
- Does not invoke the J-cost function or phi-ladder scaling.
- Does not apply when the ratio is non-positive.
- Does not extend to structures other than RecognitionEvent.
Lean usage
theorem example_use (L : Ledger) (a : ℕ) : ℝ := (L.events.map (fun e => flow_contribution e a)).sumformal statement (Lean)
136noncomputable def flow_contribution (e : RecognitionEvent) (agent : ℕ) : ℝ :=
proof body
Definition body.
137 if e.source = agent ∨ e.target = agent then Real.log e.ratio else 0
138
139/-- Flow contribution of reciprocal event negates the original -/