`zero`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Ledger
domain: RRF
line: 47 · 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 47.

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

  44}
  45
  46/-- The trivial (zero) transaction. -/
  47def zero : Transaction := fromAmount 0
  48
  49/-- Transactions form an additive structure. -/
  50def add (t₁ t₂ : Transaction) : Transaction := {
  51  debit := t₁.debit + t₂.debit,
  52  credit := t₁.credit + t₂.credit,
  53  balanced := by
  54    have h₁ := t₁.balanced
  55    have h₂ := t₂.balanced
  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

papers checked against this theorem

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