pith. machine review for the scientific record. sign in
theorem

conservation_from_balance

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.LedgerForcing
domain
Foundation
line
168 · github
papers citing
22 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 168.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

Derivations using this theorem

depends on

used by

formal source

 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
 171
 172  -- Rewrite `net_flow` as a `List.sum` of `flow_contribution`.
 173  have step_eq :
 174      ∀ (acc : ℝ) (e : RecognitionEvent),
 175        (if e.source = agent then acc + Real.log e.ratio
 176          else if e.target = agent then acc + Real.log e.ratio
 177          else acc)
 178          = acc + flow_contribution e agent := by
 179    intro acc e
 180    unfold flow_contribution
 181    by_cases hs : e.source = agent
 182    · simp [hs]
 183    · by_cases ht : e.target = agent
 184      · simp [hs, ht]
 185      · simp [hs, ht]
 186
 187  have h_foldl :
 188      ∀ acc,
 189        L.events.foldl (fun acc e =>
 190            if e.source = agent then acc + Real.log e.ratio
 191            else if e.target = agent then acc + Real.log e.ratio
 192            else acc) acc
 193          =
 194        L.events.foldl (fun acc e => acc + flow_contribution e agent) acc := by
 195    intro acc
 196    induction L.events generalizing acc with
 197    | nil =>
 198        simp