AtomicTick

formal source

  27
  28end Chain
  29
  30class AtomicTick (M : RecognitionStructure) where
  31  postedAt : Nat → M.U → Prop
  32  unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u
  33
  34structure Ledger (M : RecognitionStructure) where
  35  debit : M.U → ℤ
  36  credit : M.U → ℤ
  37
  38def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
  39
  40def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
  41  phi L (ch.last) - phi L (ch.head)
  42
  43class Conserves {M} (L : Ledger M) : Prop where
  44  conserve : ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0
  45
  46/-- ## T2 (Atomicity): unique posting per tick implies no collision at a tick. -/
  47theorem T2_atomicity {M} [AtomicTick M] :
  48  ∀ t u v, AtomicTick.postedAt (M:=M) t u → AtomicTick.postedAt (M:=M) t v → u = v := by
  49  intro t u v hu hv
  50  rcases (AtomicTick.unique_post (M:=M) t) with ⟨w, hw, huniq⟩
  51  have hu' : u = w := huniq u hu
  52  have hv' : v = w := huniq v hv
  53  exact hu'.trans hv'.symm
  54
  55theorem T3_continuity {M} (L : Ledger M) [Conserves L] :
  56  ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0 := Conserves.conserve
  57
  58end IndisputableMonolith