`Transaction`

definition

show as: view math explainer →

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

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

used by

formal source

  26/-! ## Basic Transaction -/
  27
  28/-- A single transaction: a debit and credit that must balance. -/
  29structure Transaction where
  30  /-- The debit amount (positive = outflow). -/
  31  debit : ℤ
  32  /-- The credit amount (positive = inflow). -/
  33  credit : ℤ
  34  /-- The balance constraint: debit + credit = 0. -/
  35  balanced : debit + credit = 0
  36
  37namespace Transaction
  38
  39/-- Create a balanced transaction from a single amount. -/
  40def fromAmount (amount : ℤ) : Transaction := {
  41  debit := amount,
  42  credit := -amount,
  43  balanced := by omega
  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) :

papers checked against this theorem

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