flow_contribution_reciprocal
plain-language theorem explainer
The theorem establishes that the flow contribution of a recognition event to any agent is precisely the negative of the contribution from its reciprocal event. Ledger modelers in Recognition Science cite this antisymmetry when deriving net-flow cancellation from J-symmetry. The proof proceeds by case analysis on the agent's identity as source or target, reducing via the reciprocal logarithm identity or direct ring simplification.
Claim. Let $e$ be a recognition event (source agent, target agent, positive ratio) and let $a$ be an agent. The flow contribution of $e$ at $a$ plus the flow contribution of the reciprocal event of $e$ at $a$ equals zero.
background
The module proves that J-symmetry forces double-entry ledger structure. A RecognitionEvent is the structure carrying source agent, target agent, and positive real ratio; its reciprocal swaps the agents and replaces the ratio by its inverse. Flow contribution extracts the signed logarithmic increment that the event adds to an agent's net flow when the agent is source or target.
proof idea
The proof unfolds the definitions of flow_contribution and reciprocal, then applies simp. It performs by_cases on whether the agent equals the source, rewrites with log_reciprocal_cancel when true, repeats the case on the target, and falls back to ring when the agent matches neither endpoint.
why it matters
This antisymmetry is invoked directly in conservation_from_balance to conclude that net flow vanishes at every agent once the ledger is balanced. It fills the step from J-symmetry (via the reciprocal automorphism) to the double-entry property required for conservation. The result sits inside the ledger-forcing chain that begins from the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.