`add_balanced`

proved

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Ledger
domain: RRF
line: 59 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 59.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  56    omega
  57}
  58
  59theorem add_balanced (t₁ t₂ : Transaction) :
  60    (add t₁ t₂).debit + (add t₁ t₂).credit = 0 := (add t₁ t₂).balanced
  61
  62end Transaction
  63
  64/-! ## Full Ledger -/
  65
  66/-- A ledger: a sequence of transactions that globally balance. -/
  67structure Ledger where
  68  /-- The transactions in the ledger. -/
  69  transactions : List Transaction
  70  /-- Total debit. -/
  71  total_debit : ℤ := (transactions.map (·.debit)).sum
  72  /-- Total credit. -/
  73  total_credit : ℤ := (transactions.map (·.credit)).sum
  74  /-- Global balance: total debit + total credit = 0. -/
  75  global_balance : total_debit + total_credit = 0
  76
  77namespace Ledger
  78
  79/-- The empty ledger. -/
  80def empty : Ledger := {
  81  transactions := [],
  82  total_debit := 0,
  83  total_credit := 0,
  84  global_balance := by omega
  85}
  86
  87/-- A singleton ledger. -/
  88def singleton (t : Transaction) : Ledger := {
  89  transactions := [t],

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.