Ledger

formal source

  47  exact ch.f ⟨ch.n, hlt⟩
  48end Chain
  49
  50structure Ledger (M : RecognitionStructure) where
  51  debit : M.U → ℤ
  52  credit : M.U → ℤ
  53
  54@[simp] def Ledger.Carrier {M : RecognitionStructure} (_ : Ledger M) : Type :=
  55  M.U
  56
  57def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
  58
  59def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
  60  phi L (Chain.last ch) - phi L (Chain.head ch)
  61
  62class Conserves {M} (L : Ledger M) : Prop where
  63  conserve : ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0
  64
  65lemma chainFlux_zero_of_loop {M} (L : Ledger M) [Conserves L] (ch : Chain M) (h : ch.head = ch.last) :
  66  chainFlux L ch = 0 := Conserves.conserve (L:=L) ch h
  67
  68lemma phi_zero_of_balanced {M} (L : Ledger M) (hbal : ∀ u, L.debit u = L.credit u) :
  69  ∀ u, phi L u = 0 := by
  70  intro u; simp [phi, hbal u, sub_self]
  71
  72lemma chainFlux_zero_of_balanced {M} (L : Ledger M) (ch : Chain M)
  73  (hbal : ∀ u, L.debit u = L.credit u) :
  74  chainFlux L ch = 0 := by
  75  simp [chainFlux, phi_zero_of_balanced (M:=M) L hbal]
  76
  77class AtomicTick (M : RecognitionStructure) where
  78  postedAt : Nat → M.U → Prop
  79  unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u
  80