flow_contribution_reciprocal
The theorem establishes that the flow contribution of any recognition event e to an agent equals the negative of the contribution from its reciprocal event. Ledger theorists working on conservation in the Recognition Science program cite this to obtain the antisymmetry required for net-flow cancellation. The proof proceeds by unfolding the definitions, then case analysis on whether the agent matches the source or target, reducing via log_reciprocal_cancel or ring arithmetic.
claimLet $e$ be a recognition event with source $s$, target $t$ and ratio $r > 0$. Let $e'$ be the reciprocal event obtained by swapping source and target while replacing $r$ by $1/r$. Then for any agent $a$, the flow contribution of $e$ to $a$ plus the flow contribution of $e'$ to $a$ equals zero.
background
The LedgerForcing module shows that J-symmetry induces double-entry structure on recognition events. A RecognitionEvent is a structure carrying source and target agents (natural numbers), a positive real ratio, and a positivity witness. The reciprocal operation, imported from CostAlgebra, is the automorphism that inverts the ratio and swaps the agents, satisfying the posInv and posMul axioms on positive reals.
proof idea
The proof unfolds flow_contribution and reciprocal, then performs case analysis on whether the agent equals the source or the target. In the source case it rewrites with log_reciprocal_cancel using the ratio positivity hypothesis. The target case is symmetric. When the agent matches neither endpoint both terms vanish and the identity follows by ring simplification.
why it matters in Recognition Science
This supplies the antisymmetry property invoked by the downstream conservation_from_balance theorem, which concludes that net flow is zero once the ledger is balanced. It directly instantiates the module claim that J-symmetry forces double-entry bookkeeping and connects to the T5 J-uniqueness step in the forcing chain. The downstream doc-comment records the exact strategy: balanced implies the event multiset equals its reciprocal image, so any f with f(reciprocal e) = -f(e) yields a vanishing sum.
scope and limits
- Does not derive an explicit closed-form expression for flow_contribution.
- Does not prove the balanced ledger hypothesis itself.
- Does not address continuous ratios or non-discrete agent sets.
- Does not extend the cancellation to multi-event aggregates without the balanced assumption.
formal statement (Lean)
140theorem flow_contribution_reciprocal (e : RecognitionEvent) (agent : ℕ) :
141 flow_contribution e agent + flow_contribution (reciprocal e) agent = 0 := by
proof body
Term-mode proof.
142 unfold flow_contribution reciprocal
143 simp only
144 by_cases hs : e.source = agent
145 · simp only [hs, true_or, ite_true, eq_comm, or_true]
146 rw [← log_reciprocal_cancel e.ratio_pos]
147 · by_cases ht : e.target = agent
148 · simp only [hs, ht, true_or, ite_true, or_true]
149 rw [← log_reciprocal_cancel e.ratio_pos]
150 · simp only [hs, ht, false_or, ite_false]
151 ring
152
153/-- **THEOREM (Conservation)**: In a balanced ledger, net flow is zero.
154
155 **Proof Strategy**:
156 - The balanced property says count(e) = count(reciprocal(e)) for all events
157 - This means the multiset M equals M.map reciprocal
158 - For any function f with f(reciprocal e) = -f(e), we have:
159 sum(M.map f) = sum((M.map reciprocal).map f) = sum(M.map (f ∘ reciprocal)) = -sum(M.map f)
160 - Hence sum(M.map f) = 0
161
162 The flow_contribution function satisfies f(reciprocal e) = -f(e) by flow_contribution_reciprocal.
163
164 **Technical note**: The current representation uses List.foldl which doesn't directly
165 support the multiset argument. A cleaner proof would use Multiset.sum. For now, we
166 observe that the algebraic structure guarantees conservation.
167-/