Foundation Ledger Forcing Empty Ledger Net Flow

/-- The empty ledger has zero net flow. -/
theorem empty_ledger_net_flow (agent : ℕ) : net_flow empty_ledger agent = 0 := by
  simp [net_flow, empty_ledger]

/-- The empty ledger is balanced. -/
theorem empty_ledger_balanced : balanced empty_ledger := empty_ledger.double_entry

/-- The empty ledger has zero cost. -/
theorem empty_ledger_cost : ledger_cost empty_ledger = 0 := by simp [ledger_cost, empty_ledger]

/-- **THEOREM (Conservation)**: In a balanced ledger, net flow is zero.

    **Proof Strategy**:
    - The balanced property says count(e) = count(reciprocal(e)) for all events
    - This means the multiset M equals M.map reciprocal
    - For any function f with f(reciprocal e) = -f(e), we have:
      sum(M.map f) = sum((M.map reciprocal).map f) = sum(M.map (f ∘ reciprocal)) = -sum(M.map f)
    - Hence sum(M.map f) = 0

    The flow_contribution function satisfies f(reciprocal e) = -f(e) by flow_contribution_reciprocal.

    **Technical note**: The current representation uses List.foldl which doesn't directly
    support the multiset argument. A cleaner proof would use Multiset.sum. For now, we
    observe that the algebraic structure guarantees conservation.
-/
theorem conservation_from_balance (L : Ledger) (_hbal : balanced L) (agent : ℕ) :
    net_flow L agent = 0 := by
  have hbal : balanced_list L.events := _hbal

  -- Rewrite `net_flow` as a `List.sum` of `flow_contribution`.
  have step_eq :
      ∀ (acc : ℝ) (e : RecognitionEvent),
        (if e.source = agent then acc + Real.log e.ratio
          else if e.target = agent then acc + Real.log e.ratio
          else acc)
          = acc + flow_contribution e agent := by
    intro acc e
    unfold flow_contribution
    by_cases hs : e.source = agent
    · simp [hs]
    · by_cases ht : e.target = agent
      · simp [hs, ht]
      · simp [hs, ht]

  have h_foldl :
      ∀ acc,
        L.events.foldl (fun acc e =>
            if e.source = agent then acc + Real.log e.ratio
            else if e.target = agent then acc + Real.log e.ratio
            else acc) acc
          =
        L.events.foldl (fun acc e => acc + flow_contribution e agent) acc := by
    intro acc
    induction L.events generalizing acc with
    | nil =>
        simp
    | cons e rest ih =>
        simp [List.foldl, step_eq]

  have h_foldl_sum :
      ∀ acc,
        L.events.foldl (fun acc e => acc + flow_contribution e agent) acc
          =
        acc + (L.events.map (fun e => flow_contribution e agent)).sum := by
    intro acc
    induction L.events generalizing acc with
    | nil =>
        simp
    | cons e rest ih =>
        simp [List.foldl, ih, add_assoc]

  have h_netflow :
      net_flow L agent
        = (L.events.map (fun e => flow_contribution e agent)).sum := by
    unfold net_flow
    rw [h_foldl 0]
    have := h_foldl_sum 0
    simpa using this

  -- Switch to a `Multiset` view to use the balance property as an invariance under `reciprocal`.
  let M : Multiset RecognitionEvent := (L.events : Multiset RecognitionEvent)
  let f : RecognitionEvent → ℝ := fun e => flow_contribution e agent

  have h_inj : Function.Injective reciprocal := by
    intro x y hxy
    exact (reciprocal_inj x y).1 hxy

  have hM : M = M.map reciprocal := by
    ext e
    have hcount_map : (M.map reciprocal).count e = M.count (reciprocal e) := by
      -- `count_map_eq_count'` with `x := reciprocal e` gives `(map reciprocal).count e = count (reciprocal e)`.
      simpa [M, reciprocal_reciprocal] using
        (Multiset.count_map_eq_count' reciprocal M h_inj (reciprocal e))
    have hcount_bal : M.count e = M.count (reciprocal e) := by
      -- `balanced_list` is stated in terms of `List.count`; `simp` converts to multiset counts.
      simpa [M] using (hbal e)
    calc
      M.count e = M.count (reciprocal e) := hcount_bal
      _ = (M.map reciprocal).count e := by simp [hcount_map]

  have hneg : ∀ e, f (reciprocal e) = -f e := by
    intro e
    have h := flow_contribution_reciprocal e agent
    -- `f e + f (reciprocal e) = 0`
    linarith

  have hsum_neg :
      (M.map (fun e => -f e)).sum = -((M.map f).sum) := by
    induction M using Multiset.induction_on with
    | empty =>
        simp
    | @cons a s ih =>
        simp [ih, add_comm]

  have h_sum_eq_neg : (M.map f).sum = -((M.map f).sum) := by
    have h1 : (M.map f).sum = ((M.map reciprocal).map f).sum :=
      congrArg (fun s : Multiset RecognitionEvent => (s.map f).sum) hM
    have h2 : (M.map f).sum = (M.map (fun e => f (reciprocal e))).sum := by
      simpa [Multiset.map_map, Function.comp_apply] using h1
    have h3 : (M.map f).sum = (M.map (fun e => -f e)).sum := by
      have : (fun e => f (reciprocal e)) = (fun e => -f e) := by
        funext e
        exact hneg e
      simpa [this] using h2
    exact h3.trans hsum_neg

  have h_sum_zero : (M.map f).sum = 0 := by
    linarith [h_sum_eq_neg]

  -- Finish: list sum equals the multiset sum, and the multiset sum is zero.
  rw [h_netflow]
  calc
    (L.events.map f).sum = (M.map f).sum := by simp [M]
    _ = 0 := h_sum_zero