log_reciprocal_cancel

formal source

 123/-! ## Conservation from Symmetry -/
 124
 125/-- Log reciprocal cancellation: log(r) + log(1/r) = 0. -/
 126theorem log_reciprocal_cancel {r : ℝ} (_hr : r > 0) : Real.log r + Real.log (r⁻¹) = 0 := by
 127  rw [Real.log_inv]; ring
 128
 129/-- For any event e, logs of e and reciprocal(e) sum to zero. -/
 130theorem paired_log_sum_zero (e : RecognitionEvent) :
 131    Real.log e.ratio + Real.log (reciprocal e).ratio = 0 := by
 132  simp only [reciprocal]
 133  exact log_reciprocal_cancel e.ratio_pos
 134
 135/-- Helper: net flow contribution from a single event for an agent -/
 136noncomputable def flow_contribution (e : RecognitionEvent) (agent : ℕ) : ℝ :=
 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