flow_contribution_reciprocal

formal source

 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 -/
 140theorem flow_contribution_reciprocal (e : RecognitionEvent) (agent : ℕ) :
 141    flow_contribution e agent + flow_contribution (reciprocal e) agent = 0 := by
 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-/
 168theorem conservation_from_balance (L : Ledger) (_hbal : balanced L) (agent : ℕ) :
 169    net_flow L agent = 0 := by
 170  have hbal : balanced_list L.events := _hbal