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-/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.