phi

formal source

  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
  81theorem T2_atomicity {M} [AtomicTick M] :
  82  ∀ t u v, AtomicTick.postedAt (M:=M) t u → AtomicTick.postedAt (M:=M) t v → u = v := by
  83  intro t u v hu hv
  84  rcases (AtomicTick.unique_post (M:=M) t) with ⟨w, hw, huniq⟩
  85  have huw : u = w := huniq u hu
  86  have hvw : v = w := huniq v hv
  87  exact huw.trans hvw.symm